src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 61077 06cca32aa519
parent 60956 10d463883dc2
child 62493 dd154240a53c
equal deleted inserted replaced
61076:bdc1e2f0a86a 61077:06cca32aa519
   305 fun dynamic_value_strict opts cookie ctxt postproc t =
   305 fun dynamic_value_strict opts cookie ctxt postproc t =
   306   let
   306   let
   307     fun evaluator program _ vs_ty_t deps =
   307     fun evaluator program _ vs_ty_t deps =
   308       Exn.interruptible_capture (value opts ctxt cookie)
   308       Exn.interruptible_capture (value opts ctxt cookie)
   309         (Code_Target.evaluator ctxt target program deps true vs_ty_t);
   309         (Code_Target.evaluator ctxt target program deps true vs_ty_t);
   310   in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_result o postproc) evaluator t) end;
   310   in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t) end;
   311 
   311 
   312 
   312 
   313 (** counterexample generator **)
   313 (** counterexample generator **)
   314 
   314 
   315 datatype counterexample =
   315 datatype counterexample =