# HG changeset patch
# User wenzelm
# Date 1206625270 -3600
# Node ID 6561665c5cb176420f521d115efa0c35ed1e5774
# Parent  a6cad32a27b0c298c4fe467709cedc95e7f7d803
renamed ML_Context.the_context to ML_Context.the_global_context;

diff -r a6cad32a27b0 -r 6561665c5cb1 src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Thu Mar 27 14:41:09 2008 +0100
+++ b/src/Provers/clasimp.ML	Thu Mar 27 14:41:10 2008 +0100
@@ -81,7 +81,7 @@
     Simplifier.change_simpset_of thy (fn _ => ss')
   end;
 
-fun change_clasimpset f = change_clasimpset_of (ML_Context.the_context ()) f;
+fun change_clasimpset f = change_clasimpset_of (ML_Context.the_global_context ()) f;
 fun clasimpset () = (Classical.claset (), Simplifier.simpset ());
 
 
diff -r a6cad32a27b0 -r 6561665c5cb1 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Thu Mar 27 14:41:09 2008 +0100
+++ b/src/Provers/classical.ML	Thu Mar 27 14:41:10 2008 +0100
@@ -879,12 +879,12 @@
   (fn ContextCS {swrappers, uwrappers} => make_context_cs (f (swrappers, uwrappers))));
 
 val change_claset_of = change o #1 o GlobalClaset.get;
-fun change_claset f = change_claset_of (ML_Context.the_context ()) f;
+fun change_claset f = change_claset_of (ML_Context.the_global_context ()) f;
 
 fun claset_of thy =
   let val (cs_ref, ctxt_cs) = GlobalClaset.get thy
   in context_cs (ProofContext.init thy) (! cs_ref) (ctxt_cs) end;
-val claset = claset_of o ML_Context.the_context;
+val claset = claset_of o ML_Context.the_global_context;
 
 fun CLASET tacf st = tacf (claset_of (Thm.theory_of_thm st)) st;
 fun CLASET' tacf i st = tacf (claset_of (Thm.theory_of_thm st)) i st;
diff -r a6cad32a27b0 -r 6561665c5cb1 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Thu Mar 27 14:41:09 2008 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Thu Mar 27 14:41:10 2008 +0100
@@ -201,7 +201,7 @@
     \  val name = " ^ quote name ^ ";\n\
     \  exception Arg of T;\n\
     \  val _ = Context.>> (Theory.add_oracle (name, fn (thy, Arg x) => oracle thy x));\n\
-    \  val thy = ML_Context.the_context ();\n\
+    \  val thy = ML_Context.the_global_context ();\n\
     \  val invoke_" ^ name ^ " = Thm.invoke_oracle_i thy (Sign.full_name thy name);\n\
     \in\n\
     \  fun " ^ name ^ " thy x = invoke_" ^ name ^ " (thy, Arg x);\n\
diff -r a6cad32a27b0 -r 6561665c5cb1 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Thu Mar 27 14:41:09 2008 +0100
+++ b/src/Pure/Thy/thy_info.ML	Thu Mar 27 14:41:10 2008 +0100
@@ -206,13 +206,13 @@
 val _ = ML_Context.value_antiq "theory"
   (Scan.lift Args.name
     >> (fn name => (name ^ "_thy", "ThyInfo.theory " ^ ML_Syntax.print_string name))
-  || Scan.succeed ("thy", "ML_Context.the_context ()"));
+  || Scan.succeed ("thy", "ML_Context.the_global_context ()"));
 
 val _ = ML_Context.value_antiq "theory_ref"
   (Scan.lift Args.name
     >> (fn name => (name ^ "_thy",
         "Theory.check_thy (ThyInfo.theory " ^ ML_Syntax.print_string name ^ ")"))
-  || Scan.succeed ("thy", "Theory.check_thy (ML_Context.the_context ())"));
+  || Scan.succeed ("thy", "Theory.check_thy (ML_Context.the_global_context ())"));
 
 
 
@@ -603,8 +603,6 @@
     else CRITICAL (fn () => (change_thys register; perform Update name))
   end;
 
-val _ = register_theory ProtoPure.thy;
-
 
 (* finish all theories *)
 
diff -r a6cad32a27b0 -r 6561665c5cb1 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Thu Mar 27 14:41:09 2008 +0100
+++ b/src/Pure/simplifier.ML	Thu Mar 27 14:41:10 2008 +0100
@@ -110,10 +110,10 @@
 val get_simpset = ! o GlobalSimpset.get;
 
 fun change_simpset_of thy f = CRITICAL (fn () => change (GlobalSimpset.get thy) f);
-fun change_simpset f = CRITICAL (fn () => change_simpset_of (ML_Context.the_context ()) f);
+fun change_simpset f = CRITICAL (fn () => change_simpset_of (ML_Context.the_global_context ()) f);
 
 fun simpset_of thy = MetaSimplifier.context (ProofContext.init thy) (get_simpset thy);
-val simpset = simpset_of o ML_Context.the_context;
+val simpset = simpset_of o ML_Context.the_global_context;
 
 
 fun SIMPSET tacf st = tacf (simpset_of (Thm.theory_of_thm st)) st;