src/Tools/Code/code_runtime.ML
changeset 56618 874bdedb2313
parent 56245 84fc7dfa3cd4
child 56920 d651b944c67e
     1.1 --- a/src/Tools/Code/code_runtime.ML	Thu Apr 17 14:52:23 2014 +0200
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Sat Apr 19 17:23:05 2014 +0200
     1.3 @@ -392,7 +392,7 @@
     1.4  
     1.5  fun notify_val (string, value) = 
     1.6    let
     1.7 -    val _ = #enterVal ML_Env.name_space (string, value);
     1.8 +    val _ = #enterVal ML_Env.local_name_space (string, value);
     1.9      val _ = Theory.setup (Loaded_Values.map (insert (op =) string));
    1.10    in () end;
    1.11  
    1.12 @@ -401,24 +401,24 @@
    1.13  val notifying_context : use_context =
    1.14   {tune_source = #tune_source ML_Env.local_context,
    1.15    name_space =
    1.16 -   {lookupVal    = #lookupVal ML_Env.name_space,
    1.17 -    lookupType   = #lookupType ML_Env.name_space,
    1.18 -    lookupFix    = #lookupFix ML_Env.name_space,
    1.19 -    lookupStruct = #lookupStruct ML_Env.name_space,
    1.20 -    lookupSig    = #lookupSig ML_Env.name_space,
    1.21 -    lookupFunct  = #lookupFunct ML_Env.name_space,
    1.22 +   {lookupVal    = #lookupVal ML_Env.local_name_space,
    1.23 +    lookupType   = #lookupType ML_Env.local_name_space,
    1.24 +    lookupFix    = #lookupFix ML_Env.local_name_space,
    1.25 +    lookupStruct = #lookupStruct ML_Env.local_name_space,
    1.26 +    lookupSig    = #lookupSig ML_Env.local_name_space,
    1.27 +    lookupFunct  = #lookupFunct ML_Env.local_name_space,
    1.28      enterVal     = notify_val,
    1.29      enterType    = abort,
    1.30      enterFix     = abort,
    1.31      enterStruct  = abort,
    1.32      enterSig     = abort,
    1.33      enterFunct   = abort,
    1.34 -    allVal       = #allVal ML_Env.name_space,
    1.35 -    allType      = #allType ML_Env.name_space,
    1.36 -    allFix       = #allFix ML_Env.name_space,
    1.37 -    allStruct    = #allStruct ML_Env.name_space,
    1.38 -    allSig       = #allSig ML_Env.name_space,
    1.39 -    allFunct     = #allFunct ML_Env.name_space},
    1.40 +    allVal       = #allVal ML_Env.local_name_space,
    1.41 +    allType      = #allType ML_Env.local_name_space,
    1.42 +    allFix       = #allFix ML_Env.local_name_space,
    1.43 +    allStruct    = #allStruct ML_Env.local_name_space,
    1.44 +    allSig       = #allSig ML_Env.local_name_space,
    1.45 +    allFunct     = #allFunct ML_Env.local_name_space},
    1.46    str_of_pos = #str_of_pos ML_Env.local_context,
    1.47    print = #print ML_Env.local_context,
    1.48    error = #error ML_Env.local_context};