src/Tools/Spec_Check/spec_check.ML
changeset 62493 dd154240a53c
parent 62354 fdd6989cc8a0
child 62494 b90109b2487c
     1.1 --- a/src/Tools/Spec_Check/spec_check.ML	Tue Mar 01 21:00:38 2016 +0100
     1.2 +++ b/src/Tools/Spec_Check/spec_check.ML	Tue Mar 01 21:10:29 2016 +0100
     1.3 @@ -129,13 +129,13 @@
     1.4      val return = Unsynchronized.ref "return"
     1.5      val use_context : use_context =
     1.6       {name_space = #name_space ML_Env.local_context,
     1.7 -      str_of_pos = #str_of_pos ML_Env.local_context,
     1.8 +      here = #here ML_Env.local_context,
     1.9        print = fn r => return := r,
    1.10        error = #error ML_Env.local_context}
    1.11      val _ =
    1.12        Context.setmp_thread_data (SOME (Context.Proof ctxt))
    1.13          (fn () =>
    1.14 -          Secure.use_text use_context
    1.15 +          use_text use_context
    1.16              {line = 0, file = "generated code", verbose = true, debug = false} s) ()
    1.17    in
    1.18      Gen_Construction.parse_pred (! return)
    1.19 @@ -145,7 +145,7 @@
    1.20  fun run_test ctxt s =
    1.21    Context.setmp_thread_data (SOME (Context.Proof ctxt))
    1.22      (fn () =>
    1.23 -      Secure.use_text ML_Env.local_context
    1.24 +      use_text ML_Env.local_context
    1.25          {line = 0, file = "generated code", verbose = false, debug = false} s) ();
    1.26  
    1.27  (*split input into tokens*)