1.1 --- a/src/Provers/clasimp.ML	Thu Mar 27 14:41:09 2008 +0100
     1.2 +++ b/src/Provers/clasimp.ML	Thu Mar 27 14:41:10 2008 +0100
     1.3 @@ -81,7 +81,7 @@
     1.4      Simplifier.change_simpset_of thy (fn _ => ss')
     1.5    end;
     1.6  
     1.7 -fun change_clasimpset f = change_clasimpset_of (ML_Context.the_context ()) f;
     1.8 +fun change_clasimpset f = change_clasimpset_of (ML_Context.the_global_context ()) f;
     1.9  fun clasimpset () = (Classical.claset (), Simplifier.simpset ());
    1.10  
    1.11  

     2.1 --- a/src/Provers/classical.ML	Thu Mar 27 14:41:09 2008 +0100
     2.2 +++ b/src/Provers/classical.ML	Thu Mar 27 14:41:10 2008 +0100
     2.3 @@ -879,12 +879,12 @@
     2.4    (fn ContextCS {swrappers, uwrappers} => make_context_cs (f (swrappers, uwrappers))));
     2.5  
     2.6  val change_claset_of = change o #1 o GlobalClaset.get;
     2.7 -fun change_claset f = change_claset_of (ML_Context.the_context ()) f;
     2.8 +fun change_claset f = change_claset_of (ML_Context.the_global_context ()) f;
     2.9  
    2.10  fun claset_of thy =
    2.11    let val (cs_ref, ctxt_cs) = GlobalClaset.get thy
    2.12    in context_cs (ProofContext.init thy) (! cs_ref) (ctxt_cs) end;
    2.13 -val claset = claset_of o ML_Context.the_context;
    2.14 +val claset = claset_of o ML_Context.the_global_context;
    2.15  
    2.16  fun CLASET tacf st = tacf (claset_of (Thm.theory_of_thm st)) st;
    2.17  fun CLASET' tacf i st = tacf (claset_of (Thm.theory_of_thm st)) i st;

     3.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu Mar 27 14:41:09 2008 +0100
     3.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu Mar 27 14:41:10 2008 +0100
     3.3 @@ -201,7 +201,7 @@
     3.4      \  val name = " ^ quote name ^ ";\n\
     3.5      \  exception Arg of T;\n\
     3.6      \  val _ = Context.>> (Theory.add_oracle (name, fn (thy, Arg x) => oracle thy x));\n\
     3.7 -    \  val thy = ML_Context.the_context ();\n\
     3.8 +    \  val thy = ML_Context.the_global_context ();\n\
     3.9      \  val invoke_" ^ name ^ " = Thm.invoke_oracle_i thy (Sign.full_name thy name);\n\
    3.10      \in\n\
    3.11      \  fun " ^ name ^ " thy x = invoke_" ^ name ^ " (thy, Arg x);\n\

     4.1 --- a/src/Pure/Thy/thy_info.ML	Thu Mar 27 14:41:09 2008 +0100
     4.2 +++ b/src/Pure/Thy/thy_info.ML	Thu Mar 27 14:41:10 2008 +0100
     4.3 @@ -206,13 +206,13 @@
     4.4  val _ = ML_Context.value_antiq "theory"
     4.5    (Scan.lift Args.name
     4.6      >> (fn name => (name ^ "_thy", "ThyInfo.theory " ^ ML_Syntax.print_string name))
     4.7 -  || Scan.succeed ("thy", "ML_Context.the_context ()"));
     4.8 +  || Scan.succeed ("thy", "ML_Context.the_global_context ()"));
     4.9  
    4.10  val _ = ML_Context.value_antiq "theory_ref"
    4.11    (Scan.lift Args.name
    4.12      >> (fn name => (name ^ "_thy",
    4.13          "Theory.check_thy (ThyInfo.theory " ^ ML_Syntax.print_string name ^ ")"))
    4.14 -  || Scan.succeed ("thy", "Theory.check_thy (ML_Context.the_context ())"));
    4.15 +  || Scan.succeed ("thy", "Theory.check_thy (ML_Context.the_global_context ())"));
    4.16  
    4.17  
    4.18  
    4.19 @@ -603,8 +603,6 @@
    4.20      else CRITICAL (fn () => (change_thys register; perform Update name))
    4.21    end;
    4.22  
    4.23 -val _ = register_theory ProtoPure.thy;
    4.24 -
    4.25  
    4.26  (* finish all theories *)
    4.27  

     5.1 --- a/src/Pure/simplifier.ML	Thu Mar 27 14:41:09 2008 +0100
     5.2 +++ b/src/Pure/simplifier.ML	Thu Mar 27 14:41:10 2008 +0100
     5.3 @@ -110,10 +110,10 @@
     5.4  val get_simpset = ! o GlobalSimpset.get;
     5.5  
     5.6  fun change_simpset_of thy f = CRITICAL (fn () => change (GlobalSimpset.get thy) f);
     5.7 -fun change_simpset f = CRITICAL (fn () => change_simpset_of (ML_Context.the_context ()) f);
     5.8 +fun change_simpset f = CRITICAL (fn () => change_simpset_of (ML_Context.the_global_context ()) f);
     5.9  
    5.10  fun simpset_of thy = MetaSimplifier.context (ProofContext.init thy) (get_simpset thy);
    5.11 -val simpset = simpset_of o ML_Context.the_context;
    5.12 +val simpset = simpset_of o ML_Context.the_global_context;
    5.13  
    5.14  
    5.15  fun SIMPSET tacf st = tacf (simpset_of (Thm.theory_of_thm st)) st;