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/Isar/target_context.ML
changeset 81116 0fb1e2dd4122
parent 72953 90ada01470cb 
--- a/src/Pure/Isar/target_context.ML	Fri Oct 04 23:38:04 2024 +0200
+++ b/src/Pure/Isar/target_context.ML	Sat Oct 05 14:58:36 2024 +0200
@@ -6,12 +6,12 @@
 
 signature TARGET_CONTEXT =
 sig
-  val context_begin_named_cmd: (xstring * Position.T) list -> xstring * Position.T ->
+  val context_begin_named_cmd: Bundle.xname list -> xstring * Position.T ->
     theory -> local_theory
   val end_named_cmd: local_theory -> Context.generic
   val switch_named_cmd: (xstring * Position.T) option -> Context.generic ->
     (local_theory -> Context.generic) * local_theory
-  val context_begin_nested_cmd: (xstring * Position.T) list -> Element.context list ->
+  val context_begin_nested_cmd: Bundle.xname list -> Element.context list ->
     Context.generic -> local_theory
   val end_nested_cmd: local_theory -> Context.generic
 end;
@@ -20,7 +20,7 @@
 struct
 
 fun prep_includes thy =
-  map (Bundle.check (Proof_Context.init_global thy));
+  map (Bundle.check_name (Proof_Context.init_global thy));
 
 fun context_begin_named_cmd raw_includes ("-", _) thy =
       Named_Target.init (prep_includes thy raw_includes) "" thy
@@ -44,7 +44,7 @@
       end;
 
 fun includes raw_includes lthy =
-  Bundle.includes (map (Bundle.check lthy) raw_includes) lthy;
+  Bundle.includes (map (Bundle.check_name lthy) raw_includes) lthy;
 
 fun context_begin_nested_cmd raw_includes raw_elems gthy =
   gthy
isabelle