src/Tools/Code/code_runtime.ML
changeset 62354 fdd6989cc8a0
parent 61077 06cca32aa519
child 62493 dd154240a53c
     1.1 --- a/src/Tools/Code/code_runtime.ML	Wed Feb 17 21:08:18 2016 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Wed Feb 17 23:06:24 2016 +0100
     1.3 @@ -510,8 +510,7 @@
     1.4  fun abort _ = error "Only value bindings allowed.";
     1.5  
     1.6  val notifying_context : use_context =
     1.7 - {tune_source = #tune_source ML_Env.local_context,
     1.8 -  name_space =
     1.9 + {name_space =
    1.10     {lookupVal    = #lookupVal ML_Env.local_name_space,
    1.11      lookupType   = #lookupType ML_Env.local_name_space,
    1.12      lookupFix    = #lookupFix ML_Env.local_name_space,