# HG changeset patch
# User wenzelm
# Date 1419016259 -3600
# Node ID 68ca25931dce2bd76aee59e616b7df4d9f4ecbd3
# Parent  b5e253703ebd46ed4ce04e565d8fd1eb7814a781
just one data slot per program unit;

diff -r b5e253703ebd -r 68ca25931dce src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Dec 19 20:09:31 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Dec 19 20:10:59 2014 +0100
@@ -1682,56 +1682,45 @@
 
 (* transformation for code generation *)
 
-(* FIXME just one data slot (record) per program unit *)
-
-structure Pred_Result = Proof_Data
-(
-  type T = unit -> term Predicate.pred
-  fun init _ () = raise Fail "Pred_Result"
-);
-val put_pred_result = Pred_Result.put;
-
-structure Pred_Random_Result = Proof_Data
-(
-  type T = unit -> seed -> term Predicate.pred * seed
-  fun init _ () = raise Fail "Pred_Random_Result"
-);
-val put_pred_random_result = Pred_Random_Result.put;
-
-structure Dseq_Result = Proof_Data
-(
-  type T = unit -> term Limited_Sequence.dseq
-  fun init _ () = raise Fail "Dseq_Result"
-);
-val put_dseq_result = Dseq_Result.put;
-
-structure Dseq_Random_Result = Proof_Data
+structure Data = Proof_Data
 (
-  type T = unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> term Limited_Sequence.dseq * seed
-  fun init _ () = raise Fail "Dseq_Random_Result"
+  type T =
+    (unit -> term Predicate.pred) *
+    (unit -> seed -> term Predicate.pred * seed) *
+    (unit -> term Limited_Sequence.dseq) *
+    (unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed ->
+      term Limited_Sequence.dseq * seed) *
+    (unit -> Code_Numeral.natural -> term Lazy_Sequence.lazy_sequence) *
+    (unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed ->
+      Code_Numeral.natural -> term Lazy_Sequence.lazy_sequence) *
+    (unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed ->
+      Code_Numeral.natural -> (term * Code_Numeral.natural) Lazy_Sequence.lazy_sequence);
+  val empty: T =
+   (fn () => raise Fail "pred_result",
+    fn () => raise Fail "pred_random_result",
+    fn () => raise Fail "dseq_result",
+    fn () => raise Fail "dseq_random_result",
+    fn () => raise Fail "new_dseq_result",
+    fn () => raise Fail "lseq_random_result",
+    fn () => raise Fail "lseq_random_stats_result");
+  fun init _ = empty;
 );
-val put_dseq_random_result = Dseq_Random_Result.put;
-
-structure New_Dseq_Result = Proof_Data
-(
-  type T = unit -> Code_Numeral.natural -> term Lazy_Sequence.lazy_sequence
-  fun init _ () = raise Fail "New_Dseq_Random_Result"
-);
-val put_new_dseq_result = New_Dseq_Result.put;
 
-structure Lseq_Random_Result = Proof_Data
-(
-  type T = unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> Code_Numeral.natural -> term Lazy_Sequence.lazy_sequence
-  fun init _ () = raise Fail "Lseq_Random_Result"
-);
-val put_lseq_random_result = Lseq_Random_Result.put;
+val get_pred_result = #1 o Data.get;
+val get_pred_random_result = #2 o Data.get;
+val get_dseq_result = #3 o Data.get;
+val get_dseq_random_result = #4 o Data.get;
+val get_new_dseq_result = #5 o Data.get;
+val get_lseq_random_result = #6 o Data.get;
+val get_lseq_random_stats_result = #7 o Data.get;
 
-structure Lseq_Random_Stats_Result = Proof_Data
-(
-  type T = unit -> Code_Numeral.natural -> Code_Numeral.natural -> seed -> Code_Numeral.natural -> (term * Code_Numeral.natural) Lazy_Sequence.lazy_sequence
-  fun init _ () = raise Fail "Lseq_Random_Stats_Result"
-);
-val put_lseq_random_stats_result = Lseq_Random_Stats_Result.put;
+val put_pred_result = Data.map o @{apply 7(1)} o K;
+val put_pred_random_result = Data.map o @{apply 7(2)} o K;
+val put_dseq_result = Data.map o @{apply 7(3)} o K;
+val put_dseq_random_result = Data.map o @{apply 7(4)} o K;
+val put_new_dseq_result = Data.map o @{apply 7(5)} o K;
+val put_lseq_random_result = Data.map o @{apply 7(6)} o K;
+val put_lseq_random_stats_result = Data.map o @{apply 7(7)} o K;
 
 fun dest_special_compr t =
   let
@@ -1906,24 +1895,32 @@
             val [nrandom, size, depth] = map Code_Numeral.natural_of_integer arguments
           in
             rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Limited_Sequence.yieldn k
-              (Code_Runtime.dynamic_value_strict (Dseq_Random_Result.get, put_dseq_random_result, "Predicate_Compile_Core.put_dseq_random_result")
-                ctxt NONE (fn proc => fn g => fn nrandom => fn size => fn s => g nrandom size s |>> Limited_Sequence.map proc)
+              (Code_Runtime.dynamic_value_strict
+                (get_dseq_random_result, put_dseq_random_result,
+                  "Predicate_Compile_Core.put_dseq_random_result")
+                  ctxt NONE
+                  (fn proc => fn g => fn nrandom => fn size => fn s =>
+                    g nrandom size s |>> Limited_Sequence.map proc)
                   t' [] nrandom size
                 |> Random_Engine.run)
               depth true)) ())
           end
       | DSeq =>
           rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Limited_Sequence.yieldn k
-            (Code_Runtime.dynamic_value_strict (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Core.put_dseq_result")
-              ctxt NONE Limited_Sequence.map t' []) (Code_Numeral.natural_of_integer (the_single arguments)) true)) ())
+            (Code_Runtime.dynamic_value_strict
+              (get_dseq_result, put_dseq_result, "Predicate_Compile_Core.put_dseq_result")
+              ctxt NONE Limited_Sequence.map t' [])
+            (Code_Numeral.natural_of_integer (the_single arguments)) true)) ())
       | Pos_Generator_DSeq =>
           let
             val depth = Code_Numeral.natural_of_integer (the_single arguments)
           in
             rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Lazy_Sequence.yieldn k
-              (Code_Runtime.dynamic_value_strict (New_Dseq_Result.get, put_new_dseq_result, "Predicate_Compile_Core.put_new_dseq_result")
-              ctxt NONE (fn proc => fn g => fn depth => g depth |> Lazy_Sequence.map proc)
-              t' [] depth))) ())
+              (Code_Runtime.dynamic_value_strict
+                (get_new_dseq_result, put_new_dseq_result,
+                  "Predicate_Compile_Core.put_new_dseq_result")
+                ctxt NONE (fn proc => fn g => fn depth => g depth |> Lazy_Sequence.map proc)
+                t' [] depth))) ())
           end
       | New_Pos_Random_DSeq =>
           let
@@ -1935,23 +1932,28 @@
               (split_list (TimeLimit.timeLimit time_limit
               (fn () => fst (Lazy_Sequence.yieldn k
                 (Code_Runtime.dynamic_value_strict
-                  (Lseq_Random_Stats_Result.get, put_lseq_random_stats_result, "Predicate_Compile_Core.put_lseq_random_stats_result")
+                  (get_lseq_random_stats_result, put_lseq_random_stats_result,
+                    "Predicate_Compile_Core.put_lseq_random_stats_result")
                   ctxt NONE
-                  (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
+                  (fn proc => fn g => fn nrandom => fn size => fn s => fn depth =>
+                    g nrandom size s depth
                     |> Lazy_Sequence.map (apfst proc))
                     t' [] nrandom size seed depth))) ()))
             else rpair NONE
               (TimeLimit.timeLimit time_limit (fn () => fst (Lazy_Sequence.yieldn k
                 (Code_Runtime.dynamic_value_strict
-                  (Lseq_Random_Result.get, put_lseq_random_result, "Predicate_Compile_Core.put_lseq_random_result")
-                  ctxt NONE
-                  (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
-                    |> Lazy_Sequence.map proc)
-                    t' [] nrandom size seed depth))) ())
+                  (get_lseq_random_result, put_lseq_random_result,
+                    "Predicate_Compile_Core.put_lseq_random_result")
+                    ctxt NONE
+                    (fn proc => fn g => fn nrandom => fn size => fn s => fn depth =>
+                      g nrandom size s depth
+                      |> Lazy_Sequence.map proc)
+                      t' [] nrandom size seed depth))) ())
           end
       | _ =>
           rpair NONE (TimeLimit.timeLimit time_limit (fn () => fst (Predicate.yieldn k
-            (Code_Runtime.dynamic_value_strict (Pred_Result.get, put_pred_result, "Predicate_Compile_Core.put_pred_result")
+            (Code_Runtime.dynamic_value_strict
+              (get_pred_result, put_pred_result, "Predicate_Compile_Core.put_pred_result")
               ctxt NONE Predicate.map t' []))) ()))
      handle TimeLimit.TimeOut => error "Reached timeout during execution of values"
   in ((T, ts), statistics) end;
diff -r b5e253703ebd -r 68ca25931dce src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Fri Dec 19 20:09:31 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Fri Dec 19 20:10:59 2014 +0100
@@ -40,45 +40,37 @@
 
 type seed = Random_Engine.seed;
 
-(* FIXME just one data slot (record) per program unit *)
-
-structure Pred_Result = Proof_Data
-(
-  type T = unit -> Code_Numeral.natural -> Code_Numeral.natural ->
-    Code_Numeral.natural -> seed -> term list Predicate.pred
-  fun init _ () = raise Fail "Pred_Result"
-)
-val put_pred_result = Pred_Result.put
-
-structure Dseq_Result = Proof_Data
-(
-  type T = unit -> Code_Numeral.natural -> Code_Numeral.natural ->
-    seed -> term list Limited_Sequence.dseq * seed
-  fun init _ () = raise Fail "Dseq_Result"
-)
-val put_dseq_result = Dseq_Result.put
-
-structure Lseq_Result = Proof_Data
+structure Data = Proof_Data
 (
-  type T = unit -> Code_Numeral.natural -> Code_Numeral.natural ->
-    seed -> Code_Numeral.natural -> term list Lazy_Sequence.lazy_sequence
-  fun init _ () = raise Fail "Lseq_Result"
-)
-val put_lseq_result = Lseq_Result.put
+  type T =
+    (unit -> Code_Numeral.natural -> Code_Numeral.natural ->
+      Code_Numeral.natural -> seed -> term list Predicate.pred) *
+    (unit -> Code_Numeral.natural -> Code_Numeral.natural ->
+      seed -> term list Limited_Sequence.dseq * seed) *
+    (unit -> Code_Numeral.natural -> Code_Numeral.natural ->
+      seed -> Code_Numeral.natural -> term list Lazy_Sequence.lazy_sequence) *
+    (unit -> Code_Numeral.natural -> term list Lazy_Sequence.lazy_sequence) *
+    (unit -> Code_Numeral.natural -> (bool * term list) option);
+  val empty: T =
+   (fn () => raise Fail "pred_result",
+    fn () => raise Fail "dseq_result",
+    fn () => raise Fail "lseq_result",
+    fn () => raise Fail "new_dseq_result",
+    fn () => raise Fail "cps_result");
+  fun init _ = empty;
+);
 
-structure New_Dseq_Result = Proof_Data
-(
-  type T = unit -> Code_Numeral.natural -> term list Lazy_Sequence.lazy_sequence
-  fun init _ () = raise Fail "New_Dseq_Random_Result"
-)
-val put_new_dseq_result = New_Dseq_Result.put
+val get_pred_result = #1 o Data.get;
+val get_dseq_result = #2 o Data.get;
+val get_lseq_result = #3 o Data.get;
+val get_new_dseq_result = #4 o Data.get;
+val get_cps_result = #5 o Data.get;
 
-structure CPS_Result = Proof_Data
-(
-  type T = unit -> Code_Numeral.natural -> (bool * term list) option
-  fun init _ () = raise Fail "CPS_Result"
-)
-val put_cps_result = CPS_Result.put
+val put_pred_result = Data.map o @{apply 5(1)} o K;
+val put_dseq_result = Data.map o @{apply 5(2)} o K;
+val put_lseq_result = Data.map o @{apply 5(3)} o K;
+val put_new_dseq_result = Data.map o @{apply 5(4)} o K;
+val put_cps_result = Data.map o @{apply 5(5)} o K;
 
 val target = "Quickcheck"
 
@@ -293,9 +285,11 @@
         Pos_Random_DSeq =>
           let
             val compiled_term =
-              Code_Runtime.dynamic_value_strict (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Quickcheck.put_dseq_result")
+              Code_Runtime.dynamic_value_strict
+                (get_dseq_result, put_dseq_result, "Predicate_Compile_Quickcheck.put_dseq_result")
                 (Proof_Context.init_global thy4) (SOME target)
-                (fn proc => fn g => fn n => fn size => fn s => g n size s |>> (Limited_Sequence.map o map) proc)
+                (fn proc => fn g => fn n => fn size => fn s =>
+                  g n size s |>> (Limited_Sequence.map o map) proc)
                 qc_term []
           in
             (fn size => fn nrandom => fn depth =>
@@ -306,7 +300,7 @@
           let
             val compiled_term =
               Code_Runtime.dynamic_value_strict
-                (Lseq_Result.get, put_lseq_result, "Predicate_Compile_Quickcheck.put_lseq_result")
+                (get_lseq_result, put_lseq_result, "Predicate_Compile_Quickcheck.put_lseq_result")
                 (Proof_Context.init_global thy4) (SOME target)
                 (fn proc => fn g => fn nrandom => fn size => fn s => fn depth =>
                   g nrandom size s depth |> (Lazy_Sequence.map o map) proc)
@@ -322,18 +316,20 @@
           let
             val compiled_term =
               Code_Runtime.dynamic_value_strict
-                (New_Dseq_Result.get, put_new_dseq_result, "Predicate_Compile_Quickcheck.put_new_dseq_result")
+                (get_new_dseq_result, put_new_dseq_result,
+                  "Predicate_Compile_Quickcheck.put_new_dseq_result")
                 (Proof_Context.init_global thy4) (SOME target)
                 (fn proc => fn g => fn depth => g depth |> (Lazy_Sequence.map o map) proc)
                 qc_term []
           in
-            fn size => fn nrandom => fn depth => Option.map fst (Lazy_Sequence.yield (compiled_term depth))
+            fn size => fn nrandom => fn depth =>
+              Option.map fst (Lazy_Sequence.yield (compiled_term depth))
           end
       | Pos_Generator_CPS =>
           let
             val compiled_term =
               Code_Runtime.dynamic_value_strict
-                (CPS_Result.get, put_cps_result, "Predicate_Compile_Quickcheck.put_cps_result")
+                (get_cps_result, put_cps_result, "Predicate_Compile_Quickcheck.put_cps_result")
                 (Proof_Context.init_global thy4) (SOME target)
                 (fn proc => fn g => fn depth => g depth |> Option.map (apsnd (map proc)))
                 qc_term []
@@ -343,8 +339,9 @@
        | Depth_Limited_Random =>
           let
             val compiled_term = Code_Runtime.dynamic_value_strict
-              (Pred_Result.get, put_pred_result, "Predicate_Compile_Quickcheck.put_pred_result")
-                (Proof_Context.init_global thy4) (SOME target) (fn proc => fn g => fn depth => fn nrandom => fn size => fn seed =>
+              (get_pred_result, put_pred_result, "Predicate_Compile_Quickcheck.put_pred_result")
+                (Proof_Context.init_global thy4) (SOME target)
+                  (fn proc => fn g => fn depth => fn nrandom => fn size => fn seed =>
                   g depth nrandom size seed |> (Predicate.map o map) proc)
                 qc_term []
           in
diff -r b5e253703ebd -r 68ca25931dce src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Dec 19 20:09:31 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Dec 19 20:10:59 2014 +0100
@@ -440,32 +440,30 @@
         Bound 0 $ @{term "None :: term list option"} $ return)
   in HOLogic.mk_comp (wrap, mk_validator_expr ctxt t) end
   
+
 (** generator compiliation **)
 
-(* FIXME just one data slot (record) per program unit *)
-
-structure Counterexample = Proof_Data
-(
-  type T = unit -> Code_Numeral.natural -> bool ->
-    Code_Numeral.natural -> (bool * term list) option
-  fun init _ () = raise Fail "Counterexample"
-);
-val put_counterexample = Counterexample.put;
-
-structure Counterexample_Batch = Proof_Data
+structure Data = Proof_Data
 (
-  type T = unit -> (Code_Numeral.natural -> term list option) list
-  fun init _ () = raise Fail "Counterexample"
+  type T =
+    (unit -> Code_Numeral.natural -> bool ->
+      Code_Numeral.natural -> (bool * term list) option) *
+    (unit -> (Code_Numeral.natural -> term list option) list) *
+    (unit -> (Code_Numeral.natural -> bool) list);
+  val empty: T =
+   (fn () => raise Fail "counterexample",
+    fn () => raise Fail "counterexample_batch",
+    fn () => raise Fail "validator_batch");
+  fun init _ = empty;
 );
-val put_counterexample_batch = Counterexample_Batch.put;
 
-structure Validator_Batch = Proof_Data
-(
-  type T = unit -> (Code_Numeral.natural -> bool) list
-  fun init _ () = raise Fail "Counterexample"
-);
-val put_validator_batch = Validator_Batch.put;
+val get_counterexample = #1 o Data.get;
+val get_counterexample_batch = #2 o Data.get;
+val get_validator_batch = #3 o Data.get;
 
+val put_counterexample = Data.map o @{apply 3(1)} o K;
+val put_counterexample_batch = Data.map o @{apply 3(2)} o K;
+val put_validator_batch = Data.map o @{apply 3(3)} o K;
 
 val target = "Quickcheck";
 
@@ -477,7 +475,7 @@
       else if Config.get ctxt full_support then mk_full_generator_expr else mk_generator_expr
     val t' = mk_parametric_generator_expr mk_generator_expr ctxt ts;
     val compile = Code_Runtime.dynamic_value_strict
-      (Counterexample.get, put_counterexample, "Exhaustive_Generators.put_counterexample")
+      (get_counterexample, put_counterexample, "Exhaustive_Generators.put_counterexample")
       ctxt (SOME target) (fn proc => fn g =>
         fn card => fn genuine_only => fn size => g card genuine_only size
           |> (Option.map o apsnd o map) proc) t' []
@@ -498,7 +496,7 @@
   let
     val ts' = map (fn t => mk_generator_expr ctxt (t, [])) ts;
     val compiles = Code_Runtime.dynamic_value_strict
-      (Counterexample_Batch.get, put_counterexample_batch,
+      (get_counterexample_batch, put_counterexample_batch,
         "Exhaustive_Generators.put_counterexample_batch")
       ctxt (SOME target) (fn proc => map (fn g => g #> (Option.map o map) proc))
       (HOLogic.mk_list @{typ "natural => term list option"} ts') []
@@ -516,7 +514,7 @@
     val ts' = map (mk_validator_expr ctxt) ts
   in
     Code_Runtime.dynamic_value_strict
-      (Validator_Batch.get, put_validator_batch, "Exhaustive_Generators.put_validator_batch")
+      (get_validator_batch, put_validator_batch, "Exhaustive_Generators.put_validator_batch")
       ctxt (SOME target) (K I) (HOLogic.mk_list @{typ "natural => bool"} ts') []
   end;
 
diff -r b5e253703ebd -r 68ca25931dce src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Dec 19 20:09:31 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Dec 19 20:10:59 2014 +0100
@@ -134,7 +134,7 @@
     (U', Const (@{const_name Quickcheck_Narrowing.apply},
       narrowingT U --> narrowingT T --> narrowingT U') $ u $ t)
   end
-  
+
 fun mk_sum (t, u) =
   let
     val T = fastype_of t
@@ -171,7 +171,7 @@
   in
     eqs
   end
-    
+
 fun contains_recursive_type_under_function_types xs =
   exists (fn (_, (_, _, cs)) => cs |> exists (snd #> exists (fn dT =>
     (case Old_Datatype_Aux.strip_dtyp dT of (_ :: _, Old_Datatype_Aux.DtRec _) => true | _ => false)))) xs
@@ -217,19 +217,19 @@
 fun elapsed_time description e =
   let val ({elapsed, ...}, result) = Timing.timing e ()
   in (result, (description, Time.toMilliseconds elapsed)) end
-  
+
 fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size)) ctxt cookie (code_modules, _) =
   let
     val ((is_genuine, counterexample_of), (get, put, put_ml)) = cookie
     fun message s = if quiet then () else writeln s
     fun verbose_message s = if not quiet andalso verbose then writeln s else ()
     val current_size = Unsynchronized.ref 0
-    val current_result = Unsynchronized.ref Quickcheck.empty_result 
+    val current_result = Unsynchronized.ref Quickcheck.empty_result
     val tmp_prefix = "Quickcheck_Narrowing"
     val ghc_options = Config.get ctxt ghc_options
     val with_tmp_dir =
-      if Config.get ctxt overlord then with_overlord_dir else Isabelle_System.with_tmp_dir 
-    fun run in_path = 
+      if Config.get ctxt overlord then with_overlord_dir else Isabelle_System.with_tmp_dir
+    fun run in_path =
       let
         fun mk_code_file name = Path.append in_path (Path.basic (name ^ ".hs"))
         val generatedN = Code_Target.generatedN
@@ -282,7 +282,7 @@
                     ^ " (fn () => " ^ output_value ^ ")) (ML_Context.the_generic_context ())))";
                   val ctxt' = ctxt
                     |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
-                    |> Context.proof_map (exec false ml_code);                 
+                    |> Context.proof_map (exec false ml_code);
                   val counterexample = get ctxt' ()
                 in
                   if is_genuine counterexample then
@@ -296,7 +296,7 @@
                       with_size true (k + 1))
                     end
                end
-            end 
+            end
       in with_size genuine_only 0 end
   in
     with_tmp_dir tmp_prefix run
@@ -309,44 +309,45 @@
         (Code_Target.evaluator ctxt target program deps true vs_ty_t);
   in Exn.release (Code_Thingol.dynamic_value ctxt (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 _ () = raise Fail "Counterexample"
-)
-
-datatype counterexample = Universal_Counterexample of (term * counterexample)
+datatype counterexample =
+    Universal_Counterexample of (term * counterexample)
   | Existential_Counterexample of (term * counterexample) list
   | Empty_Assignment
-  
+
 fun map_counterexample f Empty_Assignment = Empty_Assignment
   | 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
+structure Data = Proof_Data
 (
-  type T = unit -> counterexample option
-  fun init _ () = raise Fail "Counterexample"
-)
+  type T =
+    (unit -> (bool * term list) option) *
+    (unit -> counterexample option);
+  val empty: T =
+   (fn () => raise Fail "counterexample",
+    fn () => raise Fail "existential_counterexample");
+  fun init _ = empty;
+);
 
-val put_existential_counterexample = Existential_Counterexample.put
+val get_counterexample = #1 o Data.get;
+val get_existential_counterexample = #2 o Data.get;
 
-val put_counterexample = Counterexample.put
+val put_counterexample = Data.map o @{apply 2(1)} o K;
+val put_existential_counterexample = Data.map o @{apply 2(2)} o K;
 
 fun finitize_functions (xTs, t) =
   let
     val (names, boundTs) = split_list xTs
     fun mk_eval_ffun dT rT =
-      Const (@{const_name "Quickcheck_Narrowing.eval_ffun"}, 
+      Const (@{const_name "Quickcheck_Narrowing.eval_ffun"},
         Type (@{type_name "Quickcheck_Narrowing.ffun"}, [dT, rT]) --> dT --> rT)
     fun mk_eval_cfun dT rT =
-      Const (@{const_name "Quickcheck_Narrowing.eval_cfun"}, 
+      Const (@{const_name "Quickcheck_Narrowing.eval_cfun"},
         Type (@{type_name "Quickcheck_Narrowing.cfun"}, [rT]) --> dT --> rT)
     fun eval_function (Type (@{type_name fun}, [dT, rT])) =
       let
@@ -437,10 +438,10 @@
       map (fn (p, (_, (x, _))) => (x, mk_case_term ctxt p qs result)) ps
       |> map (apsnd post_process)
     end
-  
+
 fun test_term ctxt catch_code_errors (t, _) =
   let
-    fun dest_result (Quickcheck.Result r) = r 
+    fun dest_result (Quickcheck.Result r) = r
     val opts =
       ((Config.get ctxt Quickcheck.genuine_only,
        (Config.get ctxt Quickcheck.quiet, Config.get ctxt Quickcheck.verbose)),
@@ -457,12 +458,14 @@
         val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
         val (qs, prop_t) = finitize (strip_quantifiers pnf_t)
         val act = if catch_code_errors then try else (fn f => SOME o f)
-        val execute = dynamic_value_strict (true, opts)
-          ((K true, fn _ => error ""), (Existential_Counterexample.get, Existential_Counterexample.put,
-            "Narrowing_Generators.put_existential_counterexample"))
-          ctxt (apfst o Option.map o map_counterexample)
-      in  
-        case act execute (mk_property qs prop_t) of 
+        val execute =
+          dynamic_value_strict (true, opts)
+            ((K true, fn _ => error ""),
+              (get_existential_counterexample, put_existential_counterexample,
+                "Narrowing_Generators.put_existential_counterexample"))
+            ctxt (apfst o Option.map o map_counterexample)
+      in
+        case act execute (mk_property qs prop_t) of
           SOME (counterexample, result) => Quickcheck.Result
             {counterexample = Option.map (pair true o mk_terms ctxt qs) counterexample,
             evaluation_terms = Option.map (K []) counterexample,
@@ -479,16 +482,18 @@
         val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
         fun ensure_testable t =
           Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
-        fun is_genuine (SOME (true, _)) = true 
+        fun is_genuine (SOME (true, _)) = true
           | is_genuine _ = false
         val counterexample_of = Option.map (apsnd (curry (op ~~) (map fst frees) o map post_process))
         val act = if catch_code_errors then try else (fn f => SOME o f)
-        val execute = dynamic_value_strict (false, opts)
-          ((is_genuine, counterexample_of),
-            (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample"))
-          ctxt (apfst o Option.map o apsnd o map)
+        val execute =
+          dynamic_value_strict (false, opts)
+            ((is_genuine, counterexample_of),
+              (get_counterexample, put_counterexample,
+                "Narrowing_Generators.put_counterexample"))
+            ctxt (apfst o Option.map o apsnd o map)
       in
-        case act execute (ensure_testable (finitize t')) of 
+        case act execute (ensure_testable (finitize t')) of
           SOME (counterexample, result) =>
             Quickcheck.Result
              {counterexample = counterexample_of counterexample,
@@ -528,5 +533,5 @@
     #> Quickcheck_Common.datatype_interpretation @{plugin quickcheck_narrowing}
       (@{sort narrowing}, instantiate_narrowing_datatype)
     #> Context.theory_map (Quickcheck.add_tester ("narrowing", (active, test_goals))));
-    
+
 end;
diff -r b5e253703ebd -r 68ca25931dce src/HOL/Tools/Quickcheck/random_generators.ML
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Dec 19 20:09:31 2014 +0100
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Fri Dec 19 20:10:59 2014 +0100
@@ -266,23 +266,27 @@
     |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
   end;
 
+
 (** building and compiling generator expressions **)
 
-(* FIXME just one data slot (record) per program unit *)
-
-structure Counterexample = Proof_Data
+structure Data = Proof_Data
 (
-  type T = unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural -> seed -> (bool * term list) option * seed
-  fun init _ () = raise Fail "Counterexample"
+  type T =
+    (unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural -> seed ->
+      (bool * term list) option * seed) *
+    (unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural -> seed ->
+      ((bool * term list) option * (bool list * bool)) * seed);
+  val empty: T =
+   (fn () => raise Fail "counterexample",
+    fn () => raise Fail "counterexample_report");
+  fun init _ = empty;
 );
-val put_counterexample = Counterexample.put;
 
-structure Counterexample_Report = Proof_Data
-(
-  type T = unit -> Code_Numeral.natural -> bool -> Code_Numeral.natural -> seed -> ((bool * term list) option * (bool list * bool)) * seed
-  fun init _ () = raise Fail "Counterexample_Report"
-);
-val put_counterexample_report = Counterexample_Report.put;
+val get_counterexample = #1 o Data.get;
+val get_counterexample_report = #2 o Data.get;
+
+val put_counterexample = Data.map o @{apply 2(1)} o K;
+val put_counterexample_report = Data.map o @{apply 2(2)} o K;
 
 val target = "Quickcheck";
 
@@ -407,11 +411,14 @@
     if Config.get ctxt Quickcheck.report then
       let
         val t' = mk_parametric_reporting_generator_expr ctxt ts;
-        val compile = Code_Runtime.dynamic_value_strict
-          (Counterexample_Report.get, put_counterexample_report, "Random_Generators.put_counterexample_report")
-          ctxt (SOME target)
-          (fn proc => fn g => fn c => fn b => fn s => g c b s
-            #>> (apfst o Option.map o apsnd o map) proc) t' [];
+        val compile =
+          Code_Runtime.dynamic_value_strict
+            (get_counterexample_report, put_counterexample_report,
+              "Random_Generators.put_counterexample_report")
+            ctxt (SOME target)
+            (fn proc => fn g => fn c => fn b => fn s =>
+              g c b s #>> (apfst o Option.map o apsnd o map) proc)
+            t' [];
         fun single_tester c b s = compile c b s |> Random_Engine.run
         fun iterate_and_collect _ _ 0 report = (NONE, report)
           | iterate_and_collect genuine_only (card, size) j report =
@@ -429,11 +436,13 @@
     else
       let
         val t' = mk_parametric_generator_expr ctxt ts;
-        val compile = Code_Runtime.dynamic_value_strict
-          (Counterexample.get, put_counterexample, "Random_Generators.put_counterexample")
-          ctxt (SOME target)
-          (fn proc => fn g => fn c => fn b => fn s => g c b s
-            #>> (Option.map o apsnd o map) proc) t' [];
+        val compile =
+          Code_Runtime.dynamic_value_strict
+            (get_counterexample, put_counterexample, "Random_Generators.put_counterexample")
+            ctxt (SOME target)
+            (fn proc => fn g => fn c => fn b => fn s =>
+              g c b s #>> (Option.map o apsnd o map) proc)
+            t' [];
         fun single_tester c b s = compile c b s |> Random_Engine.run
         fun iterate _ _ 0 = NONE
           | iterate genuine_only (card, size) j =