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