# HG changeset patch
# User wenzelm
# Date 1201468897 -3600
# Node ID d35484265f46fd6091c694f60b856b378d0ea3ab
# Parent  d542486e39e7b8c8f876b2d7f91af7c344ddd541
use_thy: do not set implicit ML context anymore;

diff -r d542486e39e7 -r d35484265f46 NEWS
--- a/NEWS	Sun Jan 27 22:21:35 2008 +0100
+++ b/NEWS	Sun Jan 27 22:21:37 2008 +0100
@@ -13,6 +13,11 @@
 specified via 3 decimal digits (as in SML).  E.g. "foo\095bar" for
 "foo_bar".
 
+* Theory loader: use_thy (and similar operations) no longer set the
+implicit ML context, which was occasionally hard to predict and in
+conflict with concurrency.  INCOMPATIBILITY, use ML within Isar which
+provides a proper context already.
+
 
 *** Pure ***
 
diff -r d542486e39e7 -r d35484265f46 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sun Jan 27 22:21:35 2008 +0100
+++ b/src/Pure/Thy/thy_info.ML	Sun Jan 27 22:21:37 2008 +0100
@@ -485,8 +485,7 @@
 fun gen_use_thy req str =
   let val name = base_name str in
     check_unfinished warning name;
-    gen_use_thy' req Path.current str;
-    CRITICAL (fn () => ML_Context.set_context (SOME (Context.Theory (get_theory name))))
+    gen_use_thy' req Path.current str
   end;
 
 in
@@ -532,9 +531,6 @@
     val dir = master_dir'' (lookup_deps name);
     val _ = check_unfinished error name;
     val _ = if int then use_thys_dir dir parents else ();
-    (* FIXME tmp *)
-    val _ = CRITICAL (fn () =>
-      ML_Context.set_context (SOME (Context.Theory (get_theory (List.last parent_names)))));
 
     val theory = Theory.begin_theory name (map get_theory parent_names);