src/Pure/ML/ml_env.ML
changeset 62889 99c7f31615c2
parent 62876 507c90523113
child 62902 3c0f53eae166
--- a/src/Pure/ML/ml_env.ML	Wed Apr 06 14:08:57 2016 +0200
+++ b/src/Pure/ML/ml_env.ML	Wed Apr 06 16:33:33 2016 +0200
@@ -133,7 +133,7 @@
         Context.the_generic_context ()
         |> (fn context => Symtab.lookup (sel1 (#sml_tables (Env.get context))) name)
       else
-        Context.thread_data ()
+        Context.get_generic_context ()
         |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#tables (Env.get context))) name)
         |> (fn NONE => sel2 ML_Name_Space.global name | some => some);
 
@@ -142,7 +142,7 @@
         Context.the_generic_context ()
         |> (fn context => Symtab.dest (sel1 (#sml_tables (Env.get context))))
       else
-        Context.thread_data ()
+        Context.get_generic_context ()
         |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#tables (Env.get context))))
         |> append (sel2 ML_Name_Space.global ()))
       |> sort_distinct (string_ord o apply2 #1);
@@ -152,7 +152,7 @@
         Context.>> (Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
           let val sml_tables' = ap1 (Symtab.update entry) sml_tables
           in make_data (bootstrap, tables, sml_tables', breakpoints) end))
-      else if is_some (Context.thread_data ()) then
+      else if is_some (Context.get_generic_context ()) then
         Context.>> (Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
           let
             val _ = if bootstrap then sel2 ML_Name_Space.global entry else ();