# HG changeset patch
# User wenzelm
# Date 1294503288 -3600
# Node ID f6ab14e61604515cc3402c0e07e59f138f6357ad
# Parent  54a58904a598bdde86f322aeccb31e2eefcda0af
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;

diff -r 54a58904a598 -r f6ab14e61604 src/HOL/Boogie/Tools/boogie_vcs.ML
--- a/src/HOL/Boogie/Tools/boogie_vcs.ML	Sat Jan 08 16:01:51 2011 +0100
+++ b/src/HOL/Boogie/Tools/boogie_vcs.ML	Sat Jan 08 17:14:48 2011 +0100
@@ -254,7 +254,7 @@
 end
 
 
-(* the VC store *)
+(* the VC store *)  (* FIXME just one data slot (record) per program unit *)
 
 fun err_unfinished () = error "An unfinished Boogie environment is still open."
 
diff -r 54a58904a598 -r f6ab14e61604 src/HOL/Library/Eval_Witness.thy
--- a/src/HOL/Library/Eval_Witness.thy	Sat Jan 08 16:01:51 2011 +0100
+++ b/src/HOL/Library/Eval_Witness.thy	Sat Jan 08 17:14:48 2011 +0100
@@ -45,8 +45,10 @@
 instance list :: (ml_equiv) ml_equiv ..
 
 ML {*
-structure Eval_Method = Proof_Data (
+structure Eval_Method = Proof_Data
+(
   type T = unit -> bool
+  (* FIXME avoid user error with non-user text *)
   fun init _ () = error "Eval_Method"
 )
 *}
diff -r 54a58904a598 -r f6ab14e61604 src/HOL/Mirabelle/Tools/mirabelle.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Sat Jan 08 16:01:51 2011 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Sat Jan 08 17:14:48 2011 +0100
@@ -66,7 +66,7 @@
   type T = (int * run_action * done_action) list
   val empty = []
   val extend = I
-  fun merge data = Library.merge (K true) data  (* FIXME ?!? *)
+  fun merge data = Library.merge (K true) data  (* FIXME exponential blowup because of (K true) *)
 )
 
 
diff -r 54a58904a598 -r f6ab14e61604 src/HOL/Statespace/state_fun.ML
--- a/src/HOL/Statespace/state_fun.ML	Sat Jan 08 16:01:51 2011 +0100
+++ b/src/HOL/Statespace/state_fun.ML	Sat Jan 08 17:14:48 2011 +0100
@@ -101,7 +101,7 @@
   val empty = (empty_ss, empty_ss, false);
   val extend = I;
   fun merge ((ss1, ex_ss1, b1), (ss2, ex_ss2, b2)) =
-    (merge_ss (ss1, ss2), merge_ss (ex_ss1, ex_ss2), b1 orelse b2);
+    (merge_ss (ss1, ss2), merge_ss (ex_ss1, ex_ss2), b1 orelse b2 (* FIXME odd merge *));
 );
 
 val init_state_fun_data =
diff -r 54a58904a598 -r f6ab14e61604 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Sat Jan 08 16:01:51 2011 +0100
+++ b/src/HOL/Statespace/state_space.ML	Sat Jan 08 17:14:48 2011 +0100
@@ -115,7 +115,7 @@
       {declinfo=declinfo2, distinctthm=distinctthm2, silent=silent2}) : T =
     {declinfo = Termtab.merge (K true) (declinfo1, declinfo2),
      distinctthm = Symtab.merge (K true) (distinctthm1, distinctthm2),
-     silent = silent1 andalso silent2}
+     silent = silent1 andalso silent2 (* FIXME odd merge *)}
 );
 
 fun make_namespace_data declinfo distinctthm silent =
diff -r 54a58904a598 -r f6ab14e61604 src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Sat Jan 08 16:01:51 2011 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML	Sat Jan 08 17:14:48 2011 +0100
@@ -27,7 +27,7 @@
   type T = ((term * term) * thm) Symtab.table;
   val empty = Symtab.empty;
   val extend = I;
-  fun merge (a, b) = Symtab.merge (K true) (a, b);
+  fun merge data = Symtab.merge (K true) data;
 )
 
 fun init fixp mono fixp_eq phi =
diff -r 54a58904a598 -r f6ab14e61604 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Jan 08 16:01:51 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Jan 08 17:14:48 2011 +0100
@@ -275,7 +275,8 @@
 datatype boxability =
   InConstr | InSel | InExpr | InPair | InFunLHS | InFunRHS1 | InFunRHS2
 
-structure Data = Generic_Data(
+structure Data = Generic_Data
+(
   type T = {frac_types: (string * (string * string) list) list,
             codatatypes: (string * (string * styp list)) list}
   val empty = {frac_types = [], codatatypes = []}
@@ -283,7 +284,8 @@
   fun merge ({frac_types = fs1, codatatypes = cs1},
              {frac_types = fs2, codatatypes = cs2}) : T =
     {frac_types = AList.merge (op =) (K true) (fs1, fs2),
-     codatatypes = AList.merge (op =) (K true) (cs1, cs2)})
+     codatatypes = AList.merge (op =) (K true) (cs1, cs2)}
+)
 
 val name_sep = "$"
 val numeral_prefix = nitpick_prefix ^ "num" ^ name_sep
diff -r 54a58904a598 -r f6ab14e61604 src/HOL/Tools/Nitpick/nitpick_isar.ML
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sat Jan 08 16:01:51 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sat Jan 08 17:14:48 2011 +0100
@@ -130,11 +130,13 @@
             else
               [(name, value)]
 
-structure Data = Theory_Data(
+structure Data = Theory_Data
+(
   type T = raw_param list
   val empty = map (apsnd single) default_default_params
   val extend = I
-  fun merge (x, y) = AList.merge (op =) (K true) (x, y))
+  fun merge data = AList.merge (op =) (K true) data
+)
 
 val set_default_raw_param =
   Data.map o fold (AList.update (op =)) o normalize_raw_param
diff -r 54a58904a598 -r f6ab14e61604 src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Jan 08 16:01:51 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Jan 08 17:14:48 2011 +0100
@@ -63,11 +63,13 @@
 type term_postprocessor =
   Proof.context -> string -> (typ -> term list) -> typ -> term -> term
 
-structure Data = Generic_Data(
+structure Data = Generic_Data
+(
   type T = (typ * term_postprocessor) list
   val empty = []
   val extend = I
-  fun merge (x, y) = AList.merge (op =) (K true) (x, y))
+  fun merge data = AList.merge (op =) (K true) data
+)
 
 fun xsym s s' () = if print_mode_active Symbol.xsymbolsN then s else s'
 
diff -r 54a58904a598 -r f6ab14e61604 src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sat Jan 08 16:01:51 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sat Jan 08 17:14:48 2011 +0100
@@ -81,7 +81,7 @@
 fun merge_global_limit (NONE, NONE) = NONE
   | merge_global_limit (NONE, SOME n) = SOME n
   | merge_global_limit (SOME n, NONE) = SOME n
-  | merge_global_limit (SOME n, SOME m) = SOME (Int.max (n, m))
+  | merge_global_limit (SOME n, SOME m) = SOME (Int.max (n, m))  (* FIXME odd merge *)
    
 structure Options = Theory_Data
 (
@@ -96,7 +96,7 @@
      {ensure_groundness = ensure_groundness2, limit_globally = limit_globally2,
       limited_types = limited_types2, limited_predicates = limited_predicates2,
       replacing = replacing2, manual_reorder = manual_reorder2}) =
-    {ensure_groundness = ensure_groundness1 orelse ensure_groundness2,
+    {ensure_groundness = ensure_groundness1 orelse ensure_groundness2 (* FIXME odd merge *),
      limit_globally = merge_global_limit (limit_globally1, limit_globally2),
      limited_types = AList.merge (op =) (K true) (limited_types1, limited_types2),
      limited_predicates = AList.merge (op =) (K true) (limited_predicates1, limited_predicates2),
@@ -122,9 +122,7 @@
   type T = system_configuration
   val empty = {timeout = seconds 10.0, prolog_system = SWI_PROLOG}
   val extend = I;
-  fun merge ({timeout = timeout1, prolog_system = prolog_system1},
-        {timeout = timeout2, prolog_system = prolog_system2}) =
-    {timeout = timeout1, prolog_system = prolog_system1}
+  fun merge (a, _) = a
 )
 
 (* general string functions *)
diff -r 54a58904a598 -r f6ab14e61604 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Jan 08 16:01:51 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Jan 08 17:14:48 2011 +0100
@@ -1625,44 +1625,60 @@
 
 (* transformation for code generation *)
 
-structure Pred_Result = Proof_Data (
+(* FIXME just one data slot (record) per program unit *)
+
+structure Pred_Result = Proof_Data
+(
   type T = unit -> term Predicate.pred
+  (* FIXME avoid user error with non-user text *)
   fun init _ () = error "Pred_Result"
 );
 val put_pred_result = Pred_Result.put;
 
-structure Pred_Random_Result = Proof_Data (
+structure Pred_Random_Result = Proof_Data
+(
   type T = unit -> int * int -> term Predicate.pred * (int * int)
+  (* FIXME avoid user error with non-user text *)
   fun init _ () = error "Pred_Random_Result"
 );
 val put_pred_random_result = Pred_Random_Result.put;
 
-structure Dseq_Result = Proof_Data (
+structure Dseq_Result = Proof_Data
+(
   type T = unit -> term DSequence.dseq
+  (* FIXME avoid user error with non-user text *)
   fun init _ () = error "Dseq_Result"
 );
 val put_dseq_result = Dseq_Result.put;
 
-structure Dseq_Random_Result = Proof_Data (
+structure Dseq_Random_Result = Proof_Data
+(
   type T = unit -> int -> int -> int * int -> term DSequence.dseq * (int * int)
+  (* FIXME avoid user error with non-user text *)
   fun init _ () = error "Dseq_Random_Result"
 );
 val put_dseq_random_result = Dseq_Random_Result.put;
 
-structure New_Dseq_Result = Proof_Data (
+structure New_Dseq_Result = Proof_Data
+(
   type T = unit -> int -> term Lazy_Sequence.lazy_sequence
+  (* FIXME avoid user error with non-user text *)
   fun init _ () = error "New_Dseq_Random_Result"
 );
 val put_new_dseq_result = New_Dseq_Result.put;
 
-structure Lseq_Random_Result = Proof_Data (
+structure Lseq_Random_Result = Proof_Data
+(
   type T = unit -> int -> int -> int * int -> int -> term Lazy_Sequence.lazy_sequence
+  (* FIXME avoid user error with non-user text *)
   fun init _ () = error "Lseq_Random_Result"
 );
 val put_lseq_random_result = Lseq_Random_Result.put;
 
-structure Lseq_Random_Stats_Result = Proof_Data (
+structure Lseq_Random_Stats_Result = Proof_Data
+(
   type T = unit -> int -> int -> int * int -> int -> (term * int) Lazy_Sequence.lazy_sequence
+  (* FIXME avoid user error with non-user text *)
   fun init _ () = error "Lseq_Random_Stats_Result"
 );
 val put_lseq_random_stats_result = Lseq_Random_Stats_Result.put;
diff -r 54a58904a598 -r f6ab14e61604 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Sat Jan 08 16:01:51 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Sat Jan 08 17:14:48 2011 +0100
@@ -35,26 +35,36 @@
 
 open Predicate_Compile_Aux;
 
-structure Pred_Result = Proof_Data (
+(* FIXME just one data slot (record) per program unit *)
+
+structure Pred_Result = Proof_Data
+(
   type T = unit -> int -> int -> int -> int * int -> term list Predicate.pred
+  (* FIXME avoid user error with non-user text *)
   fun init _ () = error "Pred_Result"
 );
 val put_pred_result = Pred_Result.put;
 
-structure Dseq_Result = Proof_Data (
+structure Dseq_Result = Proof_Data
+(
   type T = unit -> int -> int -> int * int -> term list DSequence.dseq * (int * int)
+  (* FIXME avoid user error with non-user text *)
   fun init _ () = error "Dseq_Result"
 );
 val put_dseq_result = Dseq_Result.put;
 
-structure Lseq_Result = Proof_Data (
+structure Lseq_Result = Proof_Data
+(
   type T = unit -> int -> int -> int * int -> int -> term list Lazy_Sequence.lazy_sequence
+  (* FIXME avoid user error with non-user text *)
   fun init _ () = error "Lseq_Result"
 );
 val put_lseq_result = Lseq_Result.put;
 
-structure New_Dseq_Result = Proof_Data (
+structure New_Dseq_Result = Proof_Data
+(
   type T = unit -> int -> term list Lazy_Sequence.lazy_sequence
+  (* FIXME avoid user error with non-user text *)
   fun init _ () = error "New_Dseq_Random_Result"
 );
 val put_new_dseq_result = New_Dseq_Result.put;
diff -r 54a58904a598 -r f6ab14e61604 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Sat Jan 08 16:01:51 2011 +0100
+++ b/src/HOL/Tools/Qelim/cooper.ML	Sat Jan 08 17:14:48 2011 +0100
@@ -51,7 +51,7 @@
 (
   type T = simpset * term list;
   val empty = (HOL_ss, allowed_consts);
-  val extend  = I;
+  val extend = I;
   fun merge ((ss1, ts1), (ss2, ts2)) =
     (merge_ss (ss1, ss2), Library.merge (op aconv) (ts1, ts2));
 );
diff -r 54a58904a598 -r f6ab14e61604 src/HOL/Tools/Quotient/quotient_info.ML
--- a/src/HOL/Tools/Quotient/quotient_info.ML	Sat Jan 08 16:01:51 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_info.ML	Sat Jan 08 17:14:48 2011 +0100
@@ -55,6 +55,8 @@
 
 (** data containers **)
 
+(* FIXME just one data slot (record) per program unit *)
+
 (* info about map- and rel-functions for a type *)
 type maps_info = {mapfun: string, relmap: string}
 
diff -r 54a58904a598 -r f6ab14e61604 src/HOL/Tools/SMT/smt_config.ML
--- a/src/HOL/Tools/SMT/smt_config.ML	Sat Jan 08 16:01:51 2011 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML	Sat Jan 08 17:14:48 2011 +0100
@@ -68,7 +68,7 @@
   type T = (solver_info * string list) Symtab.table * string option
   val empty = (Symtab.empty, NONE)
   val extend = I
-  fun merge ((ss1, s), (ss2, _)) = (Symtab.merge (K true) (ss1, ss2), s)
+  fun merge ((ss1, s), (ss2, _)) = (Symtab.merge (K true) (ss1, ss2), s (* FIXME merge options!? *))
 )
 
 fun set_solver_options (name, options) =
@@ -227,7 +227,7 @@
   type T = Cache_IO.cache option
   val empty = NONE
   val extend = I
-  fun merge (s, _) = s
+  fun merge (s, _) = s  (* FIXME merge options!? *)
 )
 
 val get_certificates_path =
diff -r 54a58904a598 -r f6ab14e61604 src/HOL/Tools/SMT/smt_solver.ML
--- a/src/HOL/Tools/SMT/smt_solver.ML	Sat Jan 08 16:01:51 2011 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Sat Jan 08 17:14:48 2011 +0100
@@ -176,6 +176,7 @@
   val extend = I
   fun merge data = Symtab.merge (K true) data
     handle Symtab.DUP name => error ("Duplicate SMT solver: " ^ quote name)
+    (* FIXME never happens because of (K true) *)
 )
 
 local
diff -r 54a58904a598 -r f6ab14e61604 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Jan 08 16:01:51 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Jan 08 17:14:48 2011 +0100
@@ -133,11 +133,13 @@
                             | _ => value)
     | NONE => (name, value)
 
-structure Data = Theory_Data(
+structure Data = Theory_Data
+(
   type T = raw_param list
   val empty = default_default_params |> map (apsnd single)
   val extend = I
-  fun merge p : T = AList.merge (op =) (K true) p)
+  fun merge data : T = AList.merge (op =) (K true) data
+)
 
 fun remotify_prover_if_available_and_not_already_remote ctxt name =
   if String.isPrefix remote_prefix name then
diff -r 54a58904a598 -r f6ab14e61604 src/HOL/Tools/code_evaluation.ML
--- a/src/HOL/Tools/code_evaluation.ML	Sat Jan 08 16:01:51 2011 +0100
+++ b/src/HOL/Tools/code_evaluation.ML	Sat Jan 08 17:14:48 2011 +0100
@@ -156,8 +156,10 @@
 
 (** evaluation **)
 
-structure Evaluation = Proof_Data (
+structure Evaluation = Proof_Data
+(
   type T = unit -> term
+  (* FIXME avoid user error with non-user text *)
   fun init _ () = error "Evaluation"
 );
 val put_term = Evaluation.put;
diff -r 54a58904a598 -r f6ab14e61604 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Sat Jan 08 16:01:51 2011 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML	Sat Jan 08 17:14:48 2011 +0100
@@ -31,8 +31,9 @@
   val empty =
     {intros = Symtab.empty, graph = Graph.empty, eqns = Symtab.empty};
   val extend = I;
-  fun merge ({intros=intros1, graph=graph1, eqns=eqns1},
-    {intros=intros2, graph=graph2, eqns=eqns2}) : T =
+  fun merge
+    ({intros = intros1, graph = graph1, eqns = eqns1},
+      {intros = intros2, graph = graph2, eqns = eqns2}) : T =
     {intros = merge_rules (intros1, intros2),
      graph = Graph.merge (K true) (graph1, graph2),
      eqns = merge_rules (eqns1, eqns2)};
diff -r 54a58904a598 -r f6ab14e61604 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Sat Jan 08 16:01:51 2011 +0100
+++ b/src/HOL/Tools/inductive_set.ML	Sat Jan 08 17:14:48 2011 +0100
@@ -175,8 +175,8 @@
       set_arities = set_arities2, pred_arities = pred_arities2}) : T =
     {to_set_simps = Thm.merge_thms (to_set_simps1, to_set_simps2),
      to_pred_simps = Thm.merge_thms (to_pred_simps1, to_pred_simps2),
-     set_arities = Symtab.merge_list op = (set_arities1, set_arities2),
-     pred_arities = Symtab.merge_list op = (pred_arities1, pred_arities2)};
+     set_arities = Symtab.merge_list (op =) (set_arities1, set_arities2),
+     pred_arities = Symtab.merge_list (op =) (pred_arities1, pred_arities2)};
 );
 
 fun name_type_of (Free p) = SOME p
diff -r 54a58904a598 -r f6ab14e61604 src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Sat Jan 08 16:01:51 2011 +0100
+++ b/src/HOL/Tools/quickcheck_generators.ML	Sat Jan 08 17:14:48 2011 +0100
@@ -307,14 +307,20 @@
 
 (** building and compiling generator expressions **)
 
-structure Counterexample = Proof_Data (
+(* FIXME just one data slot (record) per program unit *)
+
+structure Counterexample = Proof_Data
+(
   type T = unit -> int -> int * int -> term list option * (int * int)
+  (* FIXME avoid user error with non-user text *)
   fun init _ () = error "Counterexample"
 );
 val put_counterexample = Counterexample.put;
 
-structure Counterexample_Report = Proof_Data (
+structure Counterexample_Report = Proof_Data
+(
   type T = unit -> int -> seed -> (term list option * (bool list * bool)) * seed
+  (* FIXME avoid user error with non-user text *)
   fun init _ () = error "Counterexample_Report"
 );
 val put_counterexample_report = Counterexample_Report.put;
diff -r 54a58904a598 -r f6ab14e61604 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Sat Jan 08 16:01:51 2011 +0100
+++ b/src/HOL/Tools/refute.ML	Sat Jan 08 17:14:48 2011 +0100
@@ -221,7 +221,7 @@
      {interpreters = in2, printers = pr2, parameters = pa2}) : T =
     {interpreters = AList.merge (op =) (K true) (in1, in2),
      printers = AList.merge (op =) (K true) (pr1, pr2),
-     parameters = Symtab.merge (op=) (pa1, pa2)};
+     parameters = Symtab.merge (op =) (pa1, pa2)};
 );
 
 val get_data = Data.get o ProofContext.theory_of;
diff -r 54a58904a598 -r f6ab14e61604 src/HOL/Tools/smallvalue_generators.ML
--- a/src/HOL/Tools/smallvalue_generators.ML	Sat Jan 08 16:01:51 2011 +0100
+++ b/src/HOL/Tools/smallvalue_generators.ML	Sat Jan 08 17:14:48 2011 +0100
@@ -210,8 +210,10 @@
 
 (** building and compiling generator expressions **)
 
-structure Counterexample = Proof_Data (
+structure Counterexample = Proof_Data
+(
   type T = unit -> int -> term list option
+  (* FIXME avoid user error with non-user text *)
   fun init _ () = error "Counterexample"
 );
 val put_counterexample = Counterexample.put;
diff -r 54a58904a598 -r f6ab14e61604 src/HOL/Tools/type_lifting.ML
--- a/src/HOL/Tools/type_lifting.ML	Sat Jan 08 16:01:51 2011 +0100
+++ b/src/HOL/Tools/type_lifting.ML	Sat Jan 08 17:14:48 2011 +0100
@@ -27,11 +27,12 @@
 type entry = { mapper: term, variances: (sort * (bool * bool)) list,
   comp: thm, id: thm };
 
-structure Data = Generic_Data(
+structure Data = Generic_Data
+(
   type T = entry list Symtab.table
   val empty = Symtab.empty
-  fun merge (xy : T * T) = Symtab.merge (K true) xy
   val extend = I
+  fun merge data = Symtab.merge (K true) data
 );
 
 val entries = Data.get o Context.Proof;
diff -r 54a58904a598 -r f6ab14e61604 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Sat Jan 08 16:01:51 2011 +0100
+++ b/src/Pure/Isar/code.ML	Sat Jan 08 17:14:48 2011 +0100
@@ -263,7 +263,7 @@
   type T = spec * (data * theory_ref) option Synchronized.var;
   val empty = (make_spec (false, (((Symtab.empty, Symtab.empty), Symtab.empty),
     (Symtab.empty, (Symtab.empty, Symtab.empty)))), empty_dataref ());
-  val extend = I
+  val extend = I  (* FIXME empty_dataref!?! *)
   fun merge ((spec1, _), (spec2, _)) =
     (merge_spec (spec1, spec2), empty_dataref ());
 );
@@ -1238,7 +1238,7 @@
 
 (** infrastructure **)
 
-(* c.f. src/HOL/Tools/recfun_codegen.ML *)
+(* cf. src/HOL/Tools/recfun_codegen.ML *)
 
 structure Code_Target_Attr = Theory_Data
 (
diff -r 54a58904a598 -r f6ab14e61604 src/Pure/Isar/spec_rules.ML
--- a/src/Pure/Isar/spec_rules.ML	Sat Jan 08 16:01:51 2011 +0100
+++ b/src/Pure/Isar/spec_rules.ML	Sat Jan 08 17:14:48 2011 +0100
@@ -37,7 +37,7 @@
         eq_list Thm.eq_thm_prop (ths1, ths2))
       (#1 o #2);
   val extend = I;
-  fun merge data = Item_Net.merge data;
+  val merge = Item_Net.merge;
 );
 
 val get = Item_Net.content o Rules.get o Context.Proof;
diff -r 54a58904a598 -r f6ab14e61604 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sat Jan 08 16:01:51 2011 +0100
+++ b/src/Pure/Isar/specification.ML	Sat Jan 08 17:14:48 2011 +0100
@@ -366,7 +366,7 @@
   type T = ((bool -> Proof.state -> Proof.state) * stamp) list;
   val empty = [];
   val extend = I;
-  fun merge hooks : T = Library.merge (eq_snd op =) hooks;
+  fun merge data : T = Library.merge (eq_snd op =) data;
 );
 
 fun gen_theorem schematic prep_att prep_stmt
diff -r 54a58904a598 -r f6ab14e61604 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Sat Jan 08 16:01:51 2011 +0100
+++ b/src/Tools/Code/code_runtime.ML	Sat Jan 08 17:14:48 2011 +0100
@@ -138,6 +138,7 @@
 structure Truth_Result = Proof_Data
 (
   type T = unit -> truth
+  (* FIXME avoid user error with non-user text *)
   fun init _ () = error "Truth_Result"
 );
 val put_truth = Truth_Result.put;
@@ -369,8 +370,8 @@
 (
   type T = string list
   val empty = []
+  val extend = I
   fun merge data : T = Library.merge (op =) data
-  val extend = I
 );
 
 fun notify_val (string, value) = 
diff -r 54a58904a598 -r f6ab14e61604 src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.ML	Sat Jan 08 16:01:51 2011 +0100
+++ b/src/Tools/adhoc_overloading.ML	Sat Jan 08 17:14:48 2011 +0100
@@ -53,10 +53,11 @@
     if ext_name1 = ext_name2 then ext_name1
     else duplicate_variant_err int_name ext_name1;
 
-  fun merge ({internalize=int1, externalize=ext1},
-      {internalize=int2, externalize=ext2}) =
-    {internalize=Symtab.join (K (Library.merge (op =))) (int1, int2),
-     externalize=Symtab.join merge_ext (ext1, ext2)};
+  fun merge
+    ({internalize = int1, externalize = ext1},
+      {internalize = int2, externalize = ext2}) : T =
+    {internalize = Symtab.join (K (Library.merge (op =))) (int1, int2),
+      externalize = Symtab.join merge_ext (ext1, ext2)};
 );
 
 fun map_tables f g =
diff -r 54a58904a598 -r f6ab14e61604 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Sat Jan 08 16:01:51 2011 +0100
+++ b/src/Tools/nbe.ML	Sat Jan 08 17:14:48 2011 +0100
@@ -229,8 +229,10 @@
 
 (* nbe specific syntax and sandbox communication *)
 
-structure Univs = Proof_Data (
+structure Univs = Proof_Data
+(
   type T = unit -> Univ list -> Univ list
+  (* FIXME avoid user error with non-user text *)
   fun init _ () = error "Univs"
 );
 val put_result = Univs.put;
diff -r 54a58904a598 -r f6ab14e61604 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Sat Jan 08 16:01:51 2011 +0100
+++ b/src/Tools/quickcheck.ML	Sat Jan 08 17:14:48 2011 +0100
@@ -93,9 +93,10 @@
 fun map_test_params' f (Test_Params {default_type, expect}) = make_test_params (f (default_type, expect));
 
 fun merge_test_params
- (Test_Params {default_type = default_type1, expect = expect1},
-  Test_Params {default_type = default_type2, expect = expect2}) =
-  make_test_params (merge (op =) (default_type1, default_type2), merge_expectation (expect1, expect2));
+  (Test_Params {default_type = default_type1, expect = expect1},
+    Test_Params {default_type = default_type2, expect = expect2}) =
+  make_test_params
+    (merge (op =) (default_type1, default_type2), merge_expectation (expect1, expect2));
 
 structure Data = Generic_Data
 (