# HG changeset patch
# User wenzelm
# Date 1206567607 -3600
# Node ID 1b624d6e91631bd6015d35ffa72736ec1fa88c57
# Parent  2780de5a1422562e12f9720bf2491daca64243f7
adapted to Context.thread_data interface;

diff -r 2780de5a1422 -r 1b624d6e9163 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed Mar 26 22:40:05 2008 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Mar 26 22:40:07 2008 +0100
@@ -200,7 +200,7 @@
     \  val oracle: theory -> T -> term = " ^ oracle ^ ";\n\
     \  val name = " ^ quote name ^ ";\n\
     \  exception Arg of T;\n\
-    \  val _ = ML_Context.>> (Theory.add_oracle (name, fn (thy, Arg x) => oracle thy x));\n\
+    \  val _ = Context.>> (Theory.add_oracle (name, fn (thy, Arg x) => oracle thy x));\n\
     \  val thy = ML_Context.the_context ();\n\
     \  val invoke_" ^ name ^ " = Thm.invoke_oracle_i thy (Sign.full_name thy name);\n\
     \in\n\
@@ -316,7 +316,7 @@
 val welcome = Toplevel.imperative (writeln o Session.welcome);
 
 val exit = Toplevel.keep (fn state =>
- (CRITICAL (fn () => ML_Context.set_context (try Toplevel.generic_theory_of state));
+ (CRITICAL (fn () => Context.set_thread_data (try Toplevel.generic_theory_of state));
   raise Toplevel.TERMINATE));
 
 val quit = Toplevel.imperative quit;
@@ -380,7 +380,7 @@
 (* use ML text *)
 
 fun use path = Toplevel.keep (fn state =>
-  ML_Context.setmp (try Toplevel.generic_theory_of state) (ThyInfo.load_file false) path);
+  Context.setmp_thread_data (try Toplevel.generic_theory_of state) (ThyInfo.load_file false) path);
 
 (*passes changes of theory context*)
 fun use_mltext_theory (txt, pos) =
@@ -633,8 +633,8 @@
 local
 
 fun present _ txt true node = OuterSyntax.check_text txt (SOME node)
-  | present f (s, _) false node =
-      ML_Context.setmp (try (Toplevel.cases_node I (Context.Proof o Proof.context_of)) node) f s;
+  | present f (s, _) false node = Context.setmp_thread_data
+      (try (Toplevel.cases_node I (Context.Proof o Proof.context_of)) node) f s;
 
 fun present_local_theory f (loc, txt) = Toplevel.present_local_theory loc (present f txt);
 fun present_proof f txt = Toplevel.print o Toplevel.present_proof (present f txt);
diff -r 2780de5a1422 -r 1b624d6e9163 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Wed Mar 26 22:40:05 2008 +0100
+++ b/src/Pure/Isar/method.ML	Wed Mar 26 22:40:07 2008 +0100
@@ -357,7 +357,7 @@
   (ML_Context.use_mltext false pos
     ("let fun tactic (ctxt: Proof.context) (facts: thm list) : tactic =\n"
       ^ txt ^ "\nin Method.set_tactic tactic end") (SOME (Context.Proof ctxt));
-    ML_Context.setmp (SOME (Context.Proof ctxt)) (! tactic_ref ctxt)));
+    Context.setmp_thread_data (SOME (Context.Proof ctxt)) (! tactic_ref ctxt)));
 
 fun tactic txt ctxt = METHOD (ml_tactic txt ctxt);
 fun raw_tactic txt ctxt = RAW_METHOD (ml_tactic txt ctxt);
diff -r 2780de5a1422 -r 1b624d6e9163 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Wed Mar 26 22:40:05 2008 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Wed Mar 26 22:40:07 2008 +0100
@@ -309,7 +309,7 @@
 (* main loop *)
 
 fun gen_loop secure do_terminate =
- (CRITICAL (fn () => ML_Context.set_context NONE);
+ (CRITICAL (fn () => Context.set_thread_data NONE);
   Toplevel.loop secure (isar do_terminate));
 
 fun gen_main secure do_terminate =
diff -r 2780de5a1422 -r 1b624d6e9163 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Wed Mar 26 22:40:05 2008 +0100
+++ b/src/Pure/Isar/proof_display.ML	Wed Mar 26 22:40:07 2008 +0100
@@ -123,7 +123,7 @@
 fun present_results ctxt ((kind, name), res) =
   if kind = "" orelse kind = Thm.internalK then ()
   else (print_results true ctxt ((kind, name), res);
-    ML_Context.setmp (SOME (Context.Proof ctxt))
+    Context.setmp_thread_data (SOME (Context.Proof ctxt))
       (Present.results kind) (name_results name res));
 
 end;
diff -r 2780de5a1422 -r 1b624d6e9163 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Wed Mar 26 22:40:05 2008 +0100
+++ b/src/Pure/Thy/thy_info.ML	Wed Mar 26 22:40:07 2008 +0100
@@ -278,7 +278,7 @@
   | provide _ _ _ NONE = NONE;
 
 fun run_file path =
-  (case Option.map (Context.theory_name o Context.the_theory) (ML_Context.get_context ()) of
+  (case Option.map (Context.theory_name o Context.the_theory) (Context.thread_data ()) of
     NONE => (ThyLoad.load_ml Path.current path; ())
   | SOME name =>
       (case lookup_deps name of