# HG changeset patch
# User wenzelm
# Date 1325170477 -3600
# Node ID ab32a87ba01a4a8d4232573f0e7a1c53cb995a85
# Parent  313be214e40a1e4d7866e5b6c59b6745e63e2bd2
comments;

diff -r 313be214e40a -r ab32a87ba01a src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Thu Dec 29 14:44:44 2011 +0100
+++ b/src/HOL/Tools/Function/function_common.ML	Thu Dec 29 15:54:37 2011 +0100
@@ -68,6 +68,7 @@
 
 (* Termination rules *)
 
+(* FIXME just one data slot (record) per program unit *)
 structure TerminationRule = Generic_Data
 (
   type T = thm list
@@ -108,6 +109,7 @@
         defname = name defname, is_partial=is_partial }
     end
 
+(* FIXME just one data slot (record) per program unit *)
 structure FunctionData = Generic_Data
 (
   type T = (term * info) Item_Net.T;
@@ -168,6 +170,7 @@
 
 (* Default Termination Prover *)
 
+(* FIXME just one data slot (record) per program unit *)
 structure TerminationProver = Generic_Data
 (
   type T = Proof.context -> tactic
@@ -321,6 +324,7 @@
     (ts, curry op ~~ bnds o Library.unflat tss, sort, cnames)
   end
 
+(* FIXME just one data slot (record) per program unit *)
 structure Preprocessor = Generic_Data
 (
   type T = preproc
diff -r 313be214e40a -r ab32a87ba01a src/HOL/Tools/Quickcheck/exhaustive_generators.ML
--- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Thu Dec 29 14:44:44 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Thu Dec 29 15:54:37 2011 +0100
@@ -428,6 +428,8 @@
   
 (** generator compiliation **)
 
+(* FIXME just one data slot (record) per program unit *)
+
 structure Counterexample = Proof_Data
 (
   type T = unit -> int -> bool -> int -> (bool * term list) option
diff -r 313be214e40a -r ab32a87ba01a src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- 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
diff -r 313be214e40a -r ab32a87ba01a src/HOL/Tools/SMT/smt_builtin.ML
--- a/src/HOL/Tools/SMT/smt_builtin.ML	Thu Dec 29 14:44:44 2011 +0100
+++ b/src/HOL/Tools/SMT/smt_builtin.ML	Thu Dec 29 15:54:37 2011 +0100
@@ -94,6 +94,7 @@
 
 (* built-in types *)
 
+(* FIXME just one data slot (record) per program unit *)
 structure Builtin_Types = Generic_Data
 (
   type T =
@@ -148,6 +149,7 @@
 
 type bfunr = string * int * term list * (term list -> term)
 
+(* FIXME just one data slot (record) per program unit *)
 structure Builtin_Funcs = Generic_Data
 (
   type T = (term list bfun, bfunr option bfun) btab
diff -r 313be214e40a -r ab32a87ba01a src/HOL/Tools/SMT/smt_config.ML
--- a/src/HOL/Tools/SMT/smt_config.ML	Thu Dec 29 14:44:44 2011 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML	Thu Dec 29 15:54:37 2011 +0100
@@ -64,6 +64,7 @@
   avail: unit -> bool,
   options: Proof.context -> string list }
 
+(* FIXME just one data slot (record) per program unit *)
 structure Solvers = Generic_Data
 (
   type T = (solver_info * string list) Symtab.table * string option
@@ -182,6 +183,7 @@
 
 (* certificates *)
 
+(* FIXME just one data slot (record) per program unit *)
 structure Certificates = Generic_Data
 (
   type T = Cache_IO.cache option