Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Pure.thy
changeset 81594 7e1b66416b7f
parent 81591 d570d215e380
child 81989 96afb0707532 
--- a/src/Pure/Pure.thy	Sat Dec 14 22:26:27 2024 +0100
+++ b/src/Pure/Pure.thy	Sat Dec 14 23:48:45 2024 +0100
@@ -408,12 +408,12 @@
       Parse.!!! (Scan.repeat1 Parse.name_position));
 
 val _ =
-  Outer_Syntax.command \<^command_keyword>\<open>syntax_consts\<close> "declare syntax const dependencies"
-    (syntax_consts >> (Toplevel.theory o Isar_Cmd.syntax_consts));
+  Outer_Syntax.local_theory \<^command_keyword>\<open>syntax_consts\<close> "declare syntax const dependencies"
+    (syntax_consts >> Isar_Cmd.syntax_consts);
 
 val _ =
-  Outer_Syntax.command \<^command_keyword>\<open>syntax_types\<close> "declare syntax const dependencies (type names)"
-    (syntax_consts >> (Toplevel.theory o Isar_Cmd.syntax_types));
+  Outer_Syntax.local_theory \<^command_keyword>\<open>syntax_types\<close> "declare syntax const dependencies (type names)"
+    (syntax_consts >> Isar_Cmd.syntax_types);
 
 val trans_pat =
   Scan.optional
isabelle