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 81113 6fefd6c602fa
parent 81106 849efff7de15
child 81136 2b949a3bfaac 
--- a/src/Pure/Pure.thy	Fri Oct 04 13:22:35 2024 +0200
+++ b/src/Pure/Pure.thy	Fri Oct 04 13:29:33 2024 +0200
@@ -654,18 +654,15 @@
 
 val _ =
   Outer_Syntax.local_theory \<^command_keyword>\<open>unbundle\<close>
-    "open bundle in local theory"
-    (Scan.repeat1 Parse.name_position >> Bundle.unbundle_cmd);
+    "open bundle in local theory" (Parse_Spec.bundles >> Bundle.unbundle_cmd);
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>include\<close>
-    "open bundle in proof body"
-    (Scan.repeat1 Parse.name_position >> (Toplevel.proof o Bundle.include_cmd));
+    "open bundle in proof body" (Parse_Spec.bundles >> (Toplevel.proof o Bundle.include_cmd));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>including\<close>
-    "open bundle in goal refinement"
-    (Scan.repeat1 Parse.name_position >> (Toplevel.proof o Bundle.including_cmd));
+    "open bundle in goal refinement" (Parse_Spec.bundles >> (Toplevel.proof o Bundle.including_cmd));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_bundles\<close>
isabelle