src/Tools/Spec_Check/spec_check.ML
changeset 62495 83db706d7771
parent 62494 b90109b2487c
child 62716 d80b9f4990e4
     1.1 --- a/src/Tools/Spec_Check/spec_check.ML	Tue Mar 01 22:11:36 2016 +0100
     1.2 +++ b/src/Tools/Spec_Check/spec_check.ML	Tue Mar 01 22:49:33 2016 +0100
     1.3 @@ -128,10 +128,10 @@
     1.4    let
     1.5      val return = Unsynchronized.ref "return"
     1.6      val context : ML_Compiler0.context =
     1.7 -     {name_space = #name_space ML_Env.local_context,
     1.8 -      here = #here ML_Env.local_context,
     1.9 +     {name_space = #name_space ML_Env.context,
    1.10 +      here = #here ML_Env.context,
    1.11        print = fn r => return := r,
    1.12 -      error = #error ML_Env.local_context}
    1.13 +      error = #error ML_Env.context}
    1.14      val _ =
    1.15        Context.setmp_thread_data (SOME (Context.Proof ctxt))
    1.16          (fn () =>
    1.17 @@ -145,7 +145,7 @@
    1.18  fun run_test ctxt s =
    1.19    Context.setmp_thread_data (SOME (Context.Proof ctxt))
    1.20      (fn () =>
    1.21 -      ML_Compiler0.use_text ML_Env.local_context
    1.22 +      ML_Compiler0.use_text ML_Env.context
    1.23          {line = 0, file = "generated code", verbose = false, debug = false} s) ();
    1.24  
    1.25  (*split input into tokens*)