1.1 --- a/src/Pure/ML/ml_antiquote.ML	Mon May 31 19:36:13 2010 +0200
     1.2 +++ b/src/Pure/ML/ml_antiquote.ML	Mon May 31 21:06:57 2010 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4  
     1.5  (* ML names *)
     1.6  
     1.7 -structure NamesData = Proof_Data
     1.8 +structure Names = Proof_Data
     1.9  (
    1.10    type T = Name.context;
    1.11    fun init _ = ML_Syntax.reserved;
    1.12 @@ -28,9 +28,9 @@
    1.13  
    1.14  fun variant a ctxt =
    1.15    let
    1.16 -    val names = NamesData.get ctxt;
    1.17 +    val names = Names.get ctxt;
    1.18      val ([b], names') = Name.variants [a] names;
    1.19 -    val ctxt' = NamesData.put names' ctxt;
    1.20 +    val ctxt' = Names.put names' ctxt;
    1.21    in (b, ctxt') end;
    1.22  
    1.23  
    1.24 @@ -64,12 +64,12 @@
    1.25      >> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name)));
    1.26  
    1.27  val _ = value "theory"
    1.28 -  (Scan.lift Args.name >> (fn name => "ThyInfo.get_theory " ^ ML_Syntax.print_string name)
    1.29 +  (Scan.lift Args.name >> (fn name => "Thy_Info.get_theory " ^ ML_Syntax.print_string name)
    1.30    || Scan.succeed "ML_Context.the_global_context ()");
    1.31  
    1.32  val _ = value "theory_ref"
    1.33    (Scan.lift Args.name >> (fn name =>
    1.34 -    "Theory.check_thy (ThyInfo.theory " ^ ML_Syntax.print_string name ^ ")")
    1.35 +    "Theory.check_thy (Thy_Info.theory " ^ ML_Syntax.print_string name ^ ")")
    1.36    || Scan.succeed "Theory.check_thy (ML_Context.the_global_context ())");
    1.37  
    1.38  val _ = value "context" (Scan.succeed "ML_Context.the_local_context ()");