src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 46042 ab32a87ba01a
parent 45923 473b744c23f2
child 46219 426ed18eba43
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Dec 29 14:44:44 2011 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Dec 29 15:54:37 2011 +0100
     1.3 @@ -313,7 +313,8 @@
     1.4    in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end;
     1.5  
     1.6  (** counterexample generator **)
     1.7 -  
     1.8 +
     1.9 +(* FIXME just one data slot (record) per program unit *)
    1.10  structure Counterexample = Proof_Data
    1.11  (
    1.12    type T = unit -> (bool * term list) option
    1.13 @@ -330,6 +331,7 @@
    1.14    | map_counterexample f (Existential_Counterexample cs) =
    1.15        Existential_Counterexample (map (fn (t, c) => (f t, map_counterexample f c)) cs)
    1.16  
    1.17 +(* FIXME just one data slot (record) per program unit *)
    1.18  structure Existential_Counterexample = Proof_Data
    1.19  (
    1.20    type T = unit -> counterexample option