src/HOL/Tools/Quickcheck/narrowing_generators.ML

       Exn.interruptible_capture (value opts ctxt cookie)
         (Code_Target.evaluator thy target naming program deps (vs_ty, t));    
   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
   fun init _ () = error "Counterexample"
 )

   | map_counterexample f (Universal_Counterexample (t, c)) =
       Universal_Counterexample (f t, map_counterexample f c)
   | 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
   fun init _ () = error "Counterexample"
 )