src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 42361 23f352990944
parent 42258 79cb339d8989
child 42616 92715b528e78
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sat Apr 16 15:47:52 2011 +0200
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sat Apr 16 16:15:37 2011 +0200
     1.3 @@ -141,7 +141,7 @@
     1.4  
     1.5  fun evaluation cookie thy evaluator vs_t args size =
     1.6    let
     1.7 -    val ctxt = ProofContext.init_global thy;
     1.8 +    val ctxt = Proof_Context.init_global thy;
     1.9      val (program_code, value_name) = evaluator vs_t;
    1.10      val value_code = space_implode " "
    1.11        (value_name :: "()" :: map (enclose "(" ")") args);
    1.12 @@ -192,7 +192,7 @@
    1.13  
    1.14  fun compile_generator_expr ctxt [(t, eval_terms)] [_, size] =
    1.15    let
    1.16 -    val thy = ProofContext.theory_of ctxt
    1.17 +    val thy = Proof_Context.theory_of ctxt
    1.18      val t' = list_abs_free (Term.add_frees t [], t)
    1.19      val t'' = if Config.get ctxt finite_functions then finitize_functions t' else t'
    1.20      fun ensure_testable t =