src/HOL/Tools/Function/function_common.ML

 val rel_name = suffix "_rel"
 val dom_name = suffix "_dom"
 
 (* Termination rules *)
 
+(* FIXME just one data slot (record) per program unit *)
 structure TerminationRule = Generic_Data
 (
   type T = thm list
   val empty = []
   val extend = I

         pinducts = fact pinducts, simps = Option.map fact simps,
         inducts = Option.map fact inducts, termination = thm termination,
         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;
   val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst);
   val extend = I;

 )
 
 
 (* Default Termination Prover *)
 
+(* FIXME just one data slot (record) per program unit *)
 structure TerminationProver = Generic_Data
 (
   type T = Proof.context -> tactic
   val empty = (fn _ => error "Termination prover not configured")
   val extend = I

     val cnames = map_index (fn (i, _) => mk_case_names i "" 1) bnds |> flat
   in
     (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
   val empty : T = empty_preproc check_defs
   val extend = I