src/Tools/Spec_Check/spec_check.ML
changeset 60956 10d463883dc2
parent 53164 beb4ee344c22
child 62354 fdd6989cc8a0
     1.1 --- a/src/Tools/Spec_Check/spec_check.ML	Mon Aug 17 15:29:30 2015 +0200
     1.2 +++ b/src/Tools/Spec_Check/spec_check.ML	Mon Aug 17 16:27:12 2015 +0200
     1.3 @@ -135,7 +135,9 @@
     1.4        error = #error ML_Env.local_context}
     1.5      val _ =
     1.6        Context.setmp_thread_data (SOME (Context.Proof ctxt))
     1.7 -        (fn () => Secure.use_text use_context (0, "generated code") true s) ()
     1.8 +        (fn () =>
     1.9 +          Secure.use_text use_context
    1.10 +            {line = 0, file = "generated code", verbose = true, debug = false} s) ()
    1.11    in
    1.12      Gen_Construction.parse_pred (! return)
    1.13    end;
    1.14 @@ -143,7 +145,9 @@
    1.15  (*call the compiler and run the test*)
    1.16  fun run_test ctxt s =
    1.17    Context.setmp_thread_data (SOME (Context.Proof ctxt))
    1.18 -    (fn () => Secure.use_text ML_Env.local_context (0, "generated code") false s) ();
    1.19 +    (fn () =>
    1.20 +      Secure.use_text ML_Env.local_context
    1.21 +        {line = 0, file = "generated code", verbose = false, debug = false} s) ();
    1.22  
    1.23  (*split input into tokens*)
    1.24  fun input_split s =