--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Dec 29 14:44:44 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Dec 29 15:54:37 2011 +0100
@@ -313,7 +313,8 @@
in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end;
(** counterexample generator **)
-
+
+(* FIXME just one data slot (record) per program unit *)
structure Counterexample = Proof_Data
(
type T = unit -> (bool * term list) option
@@ -330,6 +331,7 @@
| map_counterexample f (Existential_Counterexample cs) =
Existential_Counterexample (map (fn (t, c) => (f t, map_counterexample f c)) cs)
+(* FIXME just one data slot (record) per program unit *)
structure Existential_Counterexample = Proof_Data
(
type T = unit -> counterexample option