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