src/Pure/ML/ml_env.ML
changeset 62889 99c7f31615c2
parent 62876 507c90523113
child 62902 3c0f53eae166
     1.1 --- a/src/Pure/ML/ml_env.ML	Wed Apr 06 14:08:57 2016 +0200
     1.2 +++ b/src/Pure/ML/ml_env.ML	Wed Apr 06 16:33:33 2016 +0200
     1.3 @@ -133,7 +133,7 @@
     1.4          Context.the_generic_context ()
     1.5          |> (fn context => Symtab.lookup (sel1 (#sml_tables (Env.get context))) name)
     1.6        else
     1.7 -        Context.thread_data ()
     1.8 +        Context.get_generic_context ()
     1.9          |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#tables (Env.get context))) name)
    1.10          |> (fn NONE => sel2 ML_Name_Space.global name | some => some);
    1.11  
    1.12 @@ -142,7 +142,7 @@
    1.13          Context.the_generic_context ()
    1.14          |> (fn context => Symtab.dest (sel1 (#sml_tables (Env.get context))))
    1.15        else
    1.16 -        Context.thread_data ()
    1.17 +        Context.get_generic_context ()
    1.18          |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#tables (Env.get context))))
    1.19          |> append (sel2 ML_Name_Space.global ()))
    1.20        |> sort_distinct (string_ord o apply2 #1);
    1.21 @@ -152,7 +152,7 @@
    1.22          Context.>> (Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
    1.23            let val sml_tables' = ap1 (Symtab.update entry) sml_tables
    1.24            in make_data (bootstrap, tables, sml_tables', breakpoints) end))
    1.25 -      else if is_some (Context.thread_data ()) then
    1.26 +      else if is_some (Context.get_generic_context ()) then
    1.27          Context.>> (Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
    1.28            let
    1.29              val _ = if bootstrap then sel2 ML_Name_Space.global entry else ();