src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 55147 bce3dbc11f95
parent 51689 43a3465805dd
child 55676 fb46f1c379b5
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sat Jan 25 23:50:49 2014 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sat Jan 25 23:50:49 2014 +0100
     1.3 @@ -309,9 +309,9 @@
     1.4  fun dynamic_value_strict opts cookie thy postproc t =
     1.5    let
     1.6      val ctxt = Proof_Context.init_global thy
     1.7 -    fun evaluator naming program ((_, vs_ty), t) deps =
     1.8 +    fun evaluator program ((_, vs_ty), t) deps =
     1.9        Exn.interruptible_capture (value opts ctxt cookie)
    1.10 -        (Code_Target.evaluator thy target naming program deps (vs_ty, t));
    1.11 +        (Code_Target.evaluator thy target program deps (vs_ty, t));
    1.12    in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end;
    1.13  
    1.14  (** counterexample generator **)