--- a/src/Pure/ML/ml_antiquote.ML Mon May 31 19:36:13 2010 +0200
+++ b/src/Pure/ML/ml_antiquote.ML Mon May 31 21:06:57 2010 +0200
@@ -20,7 +20,7 @@
(* ML names *)
-structure NamesData = Proof_Data
+structure Names = Proof_Data
(
type T = Name.context;
fun init _ = ML_Syntax.reserved;
@@ -28,9 +28,9 @@
fun variant a ctxt =
let
- val names = NamesData.get ctxt;
+ val names = Names.get ctxt;
val ([b], names') = Name.variants [a] names;
- val ctxt' = NamesData.put names' ctxt;
+ val ctxt' = Names.put names' ctxt;
in (b, ctxt') end;
@@ -64,12 +64,12 @@
>> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name)));
val _ = value "theory"
- (Scan.lift Args.name >> (fn name => "ThyInfo.get_theory " ^ ML_Syntax.print_string name)
+ (Scan.lift Args.name >> (fn name => "Thy_Info.get_theory " ^ ML_Syntax.print_string name)
|| Scan.succeed "ML_Context.the_global_context ()");
val _ = value "theory_ref"
(Scan.lift Args.name >> (fn name =>
- "Theory.check_thy (ThyInfo.theory " ^ ML_Syntax.print_string name ^ ")")
+ "Theory.check_thy (Thy_Info.theory " ^ ML_Syntax.print_string name ^ ")")
|| Scan.succeed "Theory.check_thy (ML_Context.the_global_context ())");
val _ = value "context" (Scan.succeed "ML_Context.the_local_context ()");