From 032a2ecaa1574de87560dc72b3e5f7b4458fc152 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 19 Feb 2024 12:33:23 +0100
Subject: [PATCH] chore: update `builtin_widget_module` registration code

---
 src/Lean/Widget/UserWidget.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Widget/UserWidget.lean b/src/Lean/Widget/UserWidget.lean
index f110807203..d407de512c 100644
--- a/src/Lean/Widget/UserWidget.lean
+++ b/src/Lean/Widget/UserWidget.lean
@@ -102,7 +102,7 @@ builtin_initialize widgetModuleAttrImpl : AttributeImpl ←
         let env ← getEnv
         if builtin then
           let h := mkConst decl
-          declareBuiltin decl <| mkApp (mkConst ``addBuiltinModule) h
+          declareBuiltin decl <| mkApp2 (mkConst ``addBuiltinModule) (toExpr decl) h
         else
           setEnv <| moduleRegistry.addEntry env (mod.javascriptHash, decl, e)
     }