# HG changeset patch
# User wenzelm
# Date 1257702222 -3600
# Node ID 737589bb9bb8ecb89a631984e3004276b7f4d84b
# Parent  a4c54218be62b2d778c975d458e38c736b948e88
adapted Theory_Data;
tuned;

diff -r a4c54218be62 -r 737589bb9bb8 src/HOL/Boogie/Tools/boogie_split.ML
--- a/src/HOL/Boogie/Tools/boogie_split.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Boogie/Tools/boogie_split.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -18,13 +18,12 @@
 
 (* sub-tactics store *)
 
-structure Sub_Tactics = TheoryDataFun
+structure Sub_Tactics = Theory_Data
 (
   type T = (Proof.context -> int -> tactic) Symtab.table
   val empty = Symtab.empty
-  val copy = I
   val extend = I
-  fun merge _ = Symtab.merge (K true)
+  fun merge data = Symtab.merge (K true) data
 )
 
 fun add_sub_tactic tac = Sub_Tactics.map (Symtab.update_new tac)
diff -r a4c54218be62 -r 737589bb9bb8 src/HOL/Boogie/Tools/boogie_vcs.ML
--- a/src/HOL/Boogie/Tools/boogie_vcs.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Boogie/Tools/boogie_vcs.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -19,14 +19,13 @@
 
 fun err_vcs () = error "undischarged Boogie verification conditions found"
 
-structure VCs = TheoryDataFun
+structure VCs = Theory_Data
 (
-  type T = (Term.term * bool) Symtab.table option
+  type T = (term * bool) Symtab.table option
   val empty = NONE
-  val copy = I
   val extend = I
-  fun merge _ (NONE, NONE) = NONE
-    | merge _ (_, _) = err_vcs ()
+  fun merge (NONE, NONE) = NONE
+    | merge _ = err_vcs ()
 )
 
 fun set vcs = VCs.map (fn
diff -r a4c54218be62 -r 737589bb9bb8 src/HOL/Import/hol4rews.ML
--- a/src/HOL/Import/hol4rews.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Import/hol4rews.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -11,25 +11,23 @@
        | Generating of string
        | Replaying of string
 
-structure HOL4DefThy = TheoryDataFun
+structure HOL4DefThy = Theory_Data
 (
   type T = ImportStatus
   val empty = NoImport
-  val copy = I
   val extend = I
-  fun merge _ (NoImport,NoImport) = NoImport
-    | merge _ _ = (warning "Import status set during merge"; NoImport)
+  fun merge (NoImport, NoImport) = NoImport
+    | merge _ = (warning "Import status set during merge"; NoImport)
 )
 
-structure ImportSegment = TheoryDataFun
+structure ImportSegment = Theory_Data
 (
   type T = string
   val empty = ""
-  val copy = I
   val extend = I
-  fun merge _ ("",arg) = arg
-    | merge _ (arg,"") = arg
-    | merge _ (s1,s2) =
+  fun merge ("",arg) = arg
+    | merge (arg,"") = arg
+    | merge (s1,s2) =
       if s1 = s2
       then s1
       else error "Trying to merge two different import segments"
@@ -38,42 +36,38 @@
 val get_import_segment = ImportSegment.get
 val set_import_segment = ImportSegment.put
 
-structure HOL4UNames = TheoryDataFun
+structure HOL4UNames = Theory_Data
 (
   type T = string list
   val empty = []
-  val copy = I
   val extend = I
-  fun merge _ ([],[]) = []
-    | merge _ _ = error "Used names not empty during merge"
+  fun merge ([], []) = []
+    | merge _ = error "Used names not empty during merge"
 )
 
-structure HOL4Dump = TheoryDataFun
+structure HOL4Dump = Theory_Data
 (
   type T = string * string * string list
   val empty = ("","",[])
-  val copy = I
   val extend = I
-  fun merge _ (("","",[]),("","",[])) = ("","",[])
-    | merge _ _ = error "Dump data not empty during merge"
+  fun merge (("","",[]),("","",[])) = ("","",[])
+    | merge _ = error "Dump data not empty during merge"
 )
 
-structure HOL4Moves = TheoryDataFun
+structure HOL4Moves = Theory_Data
 (
   type T = string Symtab.table
   val empty = Symtab.empty
-  val copy = I
   val extend = I
-  fun merge _ : T * T -> T = Symtab.merge (K true)
+  fun merge data = Symtab.merge (K true) data
 )
 
-structure HOL4Imports = TheoryDataFun
+structure HOL4Imports = Theory_Data
 (
   type T = string Symtab.table
   val empty = Symtab.empty
-  val copy = I
   val extend = I
-  fun merge _ : T * T -> T = Symtab.merge (K true)
+  fun merge data = Symtab.merge (K true) data
 )
 
 fun get_segment2 thyname thy =
@@ -87,85 +81,76 @@
         HOL4Imports.put imps' thy
     end
 
-structure HOL4CMoves = TheoryDataFun
+structure HOL4CMoves = Theory_Data
 (
   type T = string Symtab.table
   val empty = Symtab.empty
-  val copy = I
   val extend = I
-  fun merge _ : T * T -> T = Symtab.merge (K true)
+  fun merge data = Symtab.merge (K true) data
 )
 
-structure HOL4Maps = TheoryDataFun
+structure HOL4Maps = Theory_Data
 (
-  type T = (string option) StringPair.table
+  type T = string option StringPair.table
   val empty = StringPair.empty
-  val copy = I
   val extend = I
-  fun merge _ : T * T -> T = StringPair.merge (K true)
+  fun merge data = StringPair.merge (K true) data
 )
 
-structure HOL4Thms = TheoryDataFun
+structure HOL4Thms = Theory_Data
 (
   type T = holthm StringPair.table
   val empty = StringPair.empty
-  val copy = I
   val extend = I
-  fun merge _ : T * T -> T = StringPair.merge (K true)
+  fun merge data = StringPair.merge (K true) data
 )
 
-structure HOL4ConstMaps = TheoryDataFun
+structure HOL4ConstMaps = Theory_Data
 (
   type T = (bool * string * typ option) StringPair.table
   val empty = StringPair.empty
-  val copy = I
   val extend = I
-  fun merge _ : T * T -> T = StringPair.merge (K true)
+  fun merge data = StringPair.merge (K true) data
 )
 
-structure HOL4Rename = TheoryDataFun
+structure HOL4Rename = Theory_Data
 (
   type T = string StringPair.table
   val empty = StringPair.empty
-  val copy = I
   val extend = I
-  fun merge _ : T * T -> T = StringPair.merge (K true)
+  fun merge data = StringPair.merge (K true) data
 )
 
-structure HOL4DefMaps = TheoryDataFun
+structure HOL4DefMaps = Theory_Data
 (
   type T = string StringPair.table
   val empty = StringPair.empty
-  val copy = I
   val extend = I
-  fun merge _ : T * T -> T = StringPair.merge (K true)
+  fun merge data = StringPair.merge (K true) data
 )
 
-structure HOL4TypeMaps = TheoryDataFun
+structure HOL4TypeMaps = Theory_Data
 (
   type T = (bool * string) StringPair.table
   val empty = StringPair.empty
-  val copy = I
   val extend = I
-  fun merge _ : T * T -> T = StringPair.merge (K true)
+  fun merge data = StringPair.merge (K true) data
 )
 
-structure HOL4Pending = TheoryDataFun
+structure HOL4Pending = Theory_Data
 (
   type T = ((term * term) list * thm) StringPair.table
   val empty = StringPair.empty
-  val copy = I
   val extend = I
-  fun merge _ : T * T -> T = StringPair.merge (K true)
+  fun merge data = StringPair.merge (K true) data
 )
 
-structure HOL4Rewrites = TheoryDataFun
+structure HOL4Rewrites = Theory_Data
 (
   type T = thm list
   val empty = []
-  val copy = I
   val extend = I
-  fun merge _ = Library.merge Thm.eq_thm_prop
+  val merge = Thm.merge_thms
 )
 
 val hol4_debug = Unsynchronized.ref false
diff -r a4c54218be62 -r 737589bb9bb8 src/HOL/Import/import.ML
--- a/src/HOL/Import/import.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Import/import.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -9,13 +9,12 @@
     val setup      : theory -> theory
 end
 
-structure ImportData = TheoryDataFun
+structure ImportData = Theory_Data
 (
-  type T = ProofKernel.thm option array option
+  type T = ProofKernel.thm option array option  (* FIXME mutable array !??!!! *)
   val empty = NONE
-  val copy = I
   val extend = I
-  fun merge _ _ = NONE
+  fun merge _ = NONE
 )
 
 structure Import :> IMPORT =
diff -r a4c54218be62 -r 737589bb9bb8 src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Import/shuffler.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -72,13 +72,12 @@
        | _ => raise THM("Not an equality",0,[th]))
     handle _ => raise THM("Couldn't make object equality",0,[th])  (* FIXME avoid handle _ *)
 
-structure ShuffleData = TheoryDataFun
+structure ShuffleData = Theory_Data
 (
   type T = thm list
   val empty = []
-  val copy = I
   val extend = I
-  fun merge _ = Library.merge Thm.eq_thm_prop
+  val merge = Thm.merge_thms
 )
 
 fun print_shuffles thy =
diff -r a4c54218be62 -r 737589bb9bb8 src/HOL/Mirabelle/Tools/mirabelle.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -60,13 +60,12 @@
 type run_action = int -> run_args -> unit
 type action = init_action * run_action * done_action
 
-structure Actions = TheoryDataFun
+structure Actions = Theory_Data
 (
   type T = (int * run_action * done_action) list
   val empty = []
-  val copy = I
   val extend = I
-  fun merge _ = Library.merge (K true)
+  fun merge data = Library.merge (K true) data  (* FIXME ?!? *)
 )
 
 
diff -r a4c54218be62 -r 737589bb9bb8 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -42,13 +42,12 @@
    cp_inst : thm Symtab.table,
    dj_thms : thm Symtab.table};
 
-structure NominalData = TheoryDataFun
+structure NominalData = Theory_Data
 (
   type T = atom_info Symtab.table;
   val empty = Symtab.empty;
-  val copy = I;
   val extend = I;
-  fun merge _ x = Symtab.merge (K true) x;
+  fun merge data = Symtab.merge (K true) data;
 );
 
 fun make_atom_info ((((((pt_class, fs_class), cp_classes), at_inst), pt_inst), cp_inst), dj_thms) =
diff -r a4c54218be62 -r 737589bb9bb8 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -84,13 +84,12 @@
    distinct : thm list,
    inject : thm list};
 
-structure NominalDatatypesData = TheoryDataFun
+structure NominalDatatypesData = Theory_Data
 (
   type T = nominal_datatype_info Symtab.table;
   val empty = Symtab.empty;
-  val copy = I;
   val extend = I;
-  fun merge _ tabs : T = Symtab.merge (K true) tabs;
+  fun merge data = Symtab.merge (K true) data;
 );
 
 val get_nominal_datatypes = NominalDatatypesData.get;
diff -r a4c54218be62 -r 737589bb9bb8 src/HOL/Tools/ATP_Manager/atp_manager.ML
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -226,13 +226,12 @@
 
 fun err_dup_prover name = error ("Duplicate prover: " ^ quote name);
 
-structure Provers = TheoryDataFun
+structure Provers = Theory_Data
 (
   type T = (ATP_Wrapper.prover * stamp) Symtab.table;
   val empty = Symtab.empty;
-  val copy = I;
   val extend = I;
-  fun merge _ tabs : T = Symtab.merge (eq_snd op =) tabs
+  fun merge data : T = Symtab.merge (eq_snd op =) data
     handle Symtab.DUP dup => err_dup_prover dup;
 );
 
diff -r a4c54218be62 -r 737589bb9bb8 src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -42,7 +42,7 @@
 
 (* data management *)
 
-structure DatatypesData = TheoryDataFun
+structure DatatypesData = Theory_Data
 (
   type T =
     {types: info Symtab.table,
@@ -51,11 +51,10 @@
 
   val empty =
     {types = Symtab.empty, constrs = Symtab.empty, cases = Symtab.empty};
-  val copy = I;
   val extend = I;
-  fun merge _
+  fun merge
     ({types = types1, constrs = constrs1, cases = cases1},
-     {types = types2, constrs = constrs2, cases = cases2}) =
+     {types = types2, constrs = constrs2, cases = cases2}) : T =
     {types = Symtab.merge (K true) (types1, types2),
      constrs = Symtab.join (K (AList.merge (op =) (K true))) (constrs1, constrs2),
      cases = Symtab.merge (K true) (cases1, cases2)};
diff -r a4c54218be62 -r 737589bb9bb8 src/HOL/Tools/Function/scnp_reconstruct.ML
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -63,13 +63,12 @@
    reduction_pair : thm
   }
 
-structure Multiset_Setup = TheoryDataFun
+structure Multiset_Setup = Theory_Data
 (
   type T = multiset_setup option
   val empty = NONE
-  val copy = I;
   val extend = I;
-  fun merge _ (v1, v2) = if is_some v2 then v2 else v1
+  fun merge (v1, v2) = if is_some v2 then v2 else v1   (* FIXME prefer v1 !?! *)
 )
 
 val multiset_setup = Multiset_Setup.put o SOME
diff -r a4c54218be62 -r 737589bb9bb8 src/HOL/Tools/Function/size.ML
--- a/src/HOL/Tools/Function/size.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Tools/Function/size.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -15,13 +15,12 @@
 
 open DatatypeAux;
 
-structure SizeData = TheoryDataFun
+structure SizeData = Theory_Data
 (
   type T = (string * thm list) Symtab.table;
   val empty = Symtab.empty;
-  val copy = I
   val extend = I
-  fun merge _ = Symtab.merge (K true);
+  fun merge data = Symtab.merge (K true) data;
 );
 
 val lookup_size = SizeData.get #> Symtab.lookup;
diff -r a4c54218be62 -r 737589bb9bb8 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -179,14 +179,13 @@
   unrolled_preds: unrolled list Unsynchronized.ref,
   wf_cache: wf_cache Unsynchronized.ref}
 
-structure TheoryData = TheoryDataFun(
+structure TheoryData = Theory_Data(
   type T = {frac_types: (string * (string * string) list) list,
             codatatypes: (string * (string * styp list)) list}
   val empty = {frac_types = [], codatatypes = []}
-  val copy = I
   val extend = I
-  fun merge _ ({frac_types = fs1, codatatypes = cs1},
-               {frac_types = fs2, codatatypes = cs2}) =
+  fun merge ({frac_types = fs1, codatatypes = cs1},
+               {frac_types = fs2, codatatypes = cs2}) : T =
     {frac_types = AList.merge (op =) (op =) (fs1, fs2),
      codatatypes = AList.merge (op =) (op =) (cs1, cs2)})
 
diff -r a4c54218be62 -r 737589bb9bb8 src/HOL/Tools/Nitpick/nitpick_isar.ML
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -125,13 +125,12 @@
                           | _ => value)
   | NONE => (name, value)
 
-structure TheoryData = TheoryDataFun(
+structure TheoryData = Theory_Data(
   type T = {params: raw_param list, registered_auto: bool}
   val empty = {params = rev default_default_params, registered_auto = false}
-  val copy = I
   val extend = I
-  fun merge _ ({params = ps1, registered_auto = a1},
-               {params = ps2, registered_auto = a2}) =
+  fun merge ({params = ps1, registered_auto = a1},
+               {params = ps2, registered_auto = a2}) : T =
     {params = AList.merge (op =) (op =) (ps1, ps2),
      registered_auto = a1 orelse a2})
 
diff -r a4c54218be62 -r 737589bb9bb8 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -232,13 +232,12 @@
   eq_option (Thm.eq_thm) (#elim d1, #elim d2) andalso
   #nparams d1 = #nparams d2
 
-structure PredData = TheoryDataFun
+structure PredData = Theory_Data
 (
   type T = pred_data Graph.T;
   val empty = Graph.empty;
-  val copy = I;
   val extend = I;
-  fun merge _ = Graph.merge eq_pred_data;
+  val merge = Graph.merge eq_pred_data;
 );
 
 (* queries *)
@@ -2450,7 +2449,7 @@
   (*FIXME name discrepancy in attribs and ML code*)
   (*FIXME intros should be better named intro*)
 
-(* TODO: make TheoryDataFun to Generic_Data & remove duplication of local theory and theory *)
+(* TODO: make Theory_Data to Generic_Data & remove duplication of local theory and theory *)
 fun generic_code_pred prep_const options raw_const lthy =
   let
     val thy = ProofContext.theory_of lthy
diff -r a4c54218be62 -r 737589bb9bb8 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -19,15 +19,14 @@
 
 open Predicate_Compile_Aux;
 
-structure Data = TheoryDataFun
+structure Data = Theory_Data
 (
   type T =
     {const_spec_table : thm list Symtab.table};
   val empty =
     {const_spec_table = Symtab.empty};
-  val copy = I;
   val extend = I;
-  fun merge _
+  fun merge
     ({const_spec_table = const_spec_table1},
      {const_spec_table = const_spec_table2}) =
      {const_spec_table = Symtab.merge (K true) (const_spec_table1, const_spec_table2)}
diff -r a4c54218be62 -r 737589bb9bb8 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -56,13 +56,12 @@
 fun is_constr thy = is_some o Code.get_datatype_of_constr thy;
 
 (* Table from constant name (string) to term of inductive predicate *)
-structure Pred_Compile_Preproc = TheoryDataFun
+structure Pred_Compile_Preproc = Theory_Data
 (
   type T = string Symtab.table;
   val empty = Symtab.empty;
-  val copy = I;
   val extend = I;
-  fun merge _ = Symtab.merge (op =);
+  fun merge data : T = Symtab.merge (op =) data;   (* FIXME handle Symtab.DUP ?? *)
 )
 
 fun pred_of_function thy name = Symtab.lookup (Pred_Compile_Preproc.get thy) name
diff -r a4c54218be62 -r 737589bb9bb8 src/HOL/Tools/arith_data.ML
--- a/src/HOL/Tools/arith_data.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Tools/arith_data.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -41,13 +41,12 @@
 
 val get_arith_facts = Arith_Facts.get;
 
-structure Arith_Tactics = TheoryDataFun
+structure Arith_Tactics = Theory_Data
 (
   type T = (serial * (string * (bool -> Proof.context -> int -> tactic))) list;
   val empty = [];
-  val copy = I;
   val extend = I;
-  fun merge _ = AList.merge (op =) (K true);
+  fun merge data : T = AList.merge (op =) (K true) data;
 );
 
 fun add_tactic name tac = Arith_Tactics.map (cons (serial (), (name, tac)));
diff -r a4c54218be62 -r 737589bb9bb8 src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -20,7 +20,7 @@
 fun merge_rules tabs =
   Symtab.join (fn _ => AList.merge (Thm.eq_thm_prop) (K true)) tabs;
 
-structure CodegenData = TheoryDataFun
+structure CodegenData = Theory_Data
 (
   type T =
     {intros : (thm * (string * int)) list Symtab.table,
@@ -28,10 +28,9 @@
      eqns : (thm * string) list Symtab.table};
   val empty =
     {intros = Symtab.empty, graph = Graph.empty, eqns = Symtab.empty};
-  val copy = I;
   val extend = I;
-  fun merge _ ({intros=intros1, graph=graph1, eqns=eqns1},
-    {intros=intros2, graph=graph2, eqns=eqns2}) =
+  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 a4c54218be62 -r 737589bb9bb8 src/HOL/Tools/recdef.ML
--- a/src/HOL/Tools/recdef.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Tools/recdef.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -86,18 +86,17 @@
 
 type recdef_info = {simps: thm list, rules: thm list list, induct: thm, tcs: term list};
 
-structure GlobalRecdefData = TheoryDataFun
+structure GlobalRecdefData = Theory_Data
 (
   type T = recdef_info Symtab.table * hints;
   val empty = (Symtab.empty, mk_hints ([], [], [])): T;
-  val copy = I;
   val extend = I;
-  fun merge _
+  fun merge
    ((tab1, {simps = simps1, congs = congs1, wfs = wfs1}),
     (tab2, {simps = simps2, congs = congs2, wfs = wfs2})) : T =
       (Symtab.merge (K true) (tab1, tab2),
         mk_hints (Thm.merge_thms (simps1, simps2),
-          AList.merge (op =) Thm.eq_thm (congs1, congs2),
+          AList.merge (op =) Thm.eq_thm_prop (congs1, congs2),
           Thm.merge_thms (wfs1, wfs2)));
 );
 
diff -r a4c54218be62 -r 737589bb9bb8 src/HOL/Tools/recfun_codegen.ML
--- a/src/HOL/Tools/recfun_codegen.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Tools/recfun_codegen.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -16,13 +16,12 @@
 
 val const_of = dest_Const o head_of o fst o Logic.dest_equals;
 
-structure ModuleData = TheoryDataFun
+structure ModuleData = Theory_Data
 (
   type T = string Symtab.table;
   val empty = Symtab.empty;
-  val copy = I;
   val extend = I;
-  fun merge _ = Symtab.merge (K true);
+  fun merge data = Symtab.merge (K true) data;
 );
 
 fun add_thm_target module_name thm thy =
diff -r a4c54218be62 -r 737589bb9bb8 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Tools/record.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -81,13 +81,12 @@
     cterm_instantiate (map (apfst getvar) values) thm
   end;
 
-structure IsTupleThms = TheoryDataFun
+structure IsTupleThms = Theory_Data
 (
   type T = thm Symtab.table;
   val empty = Symtab.make [tuple_istuple];
-  val copy = I;
   val extend = I;
-  fun merge _ = Symtab.merge Thm.eq_thm_prop;
+  fun merge data = Symtab.merge Thm.eq_thm_prop data;   (* FIXME handle Symtab.DUP ?? *)
 );
 
 fun do_typedef name repT alphas thy =
@@ -381,7 +380,7 @@
   equalities = equalities, extinjects=extinjects, extsplit = extsplit, splits = splits,
   extfields = extfields, fieldext = fieldext }: record_data;
 
-structure RecordsData = TheoryDataFun
+structure RecordsData = Theory_Data
 (
   type T = record_data;
   val empty =
@@ -390,10 +389,8 @@
           simpset = HOL_basic_ss, defset = HOL_basic_ss,
           foldcong = HOL_basic_ss, unfoldcong = HOL_basic_ss}
        Symtab.empty [] Symtab.empty Symtab.empty Symtab.empty Symtab.empty;
-
-  val copy = I;
   val extend = I;
-  fun merge _
+  fun merge
    ({records = recs1,
      sel_upd =
       {selectors = sels1, updates = upds1,
@@ -425,7 +422,7 @@
         foldcong = Simplifier.merge_ss (fc1, fc2),
         unfoldcong = Simplifier.merge_ss (uc1, uc2)}
       (Symtab.merge Thm.eq_thm_prop (equalities1, equalities2))
-      (Library.merge Thm.eq_thm_prop (extinjects1, extinjects2))
+      (Thm.merge_thms (extinjects1, extinjects2))
       (Symtab.merge Thm.eq_thm_prop (extsplit1, extsplit2))
       (Symtab.merge (fn ((a, b, c, d), (w, x, y, z)) =>
           Thm.eq_thm (a, w) andalso Thm.eq_thm (b, x) andalso
diff -r a4c54218be62 -r 737589bb9bb8 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Tools/refute.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -201,7 +201,7 @@
     };
 
 
-  structure RefuteData = TheoryDataFun
+  structure RefuteData = Theory_Data
   (
     type T =
       {interpreters: (string * (theory -> model -> arguments -> term ->
@@ -210,11 +210,10 @@
         (int -> bool) -> term option)) list,
        parameters: string Symtab.table};
     val empty = {interpreters = [], printers = [], parameters = Symtab.empty};
-    val copy = I;
     val extend = I;
-    fun merge _
+    fun merge
       ({interpreters = in1, printers = pr1, parameters = pa1},
-       {interpreters = in2, printers = pr2, parameters = pa2}) =
+       {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)};
diff -r a4c54218be62 -r 737589bb9bb8 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -349,13 +349,12 @@
 
 (*The cache prevents repeated clausification of a theorem, and also repeated declaration of
   Skolem functions.*)
-structure ThmCache = TheoryDataFun
+structure ThmCache = Theory_Data
 (
   type T = thm list Thmtab.table * unit Symtab.table;
   val empty = (Thmtab.empty, Symtab.empty);
-  val copy = I;
   val extend = I;
-  fun merge _ ((cache1, seen1), (cache2, seen2)) : T =
+  fun merge ((cache1, seen1), (cache2, seen2)) : T =
     (Thmtab.merge (K true) (cache1, cache2), Symtab.merge (K true) (seen1, seen2));
 );
 
diff -r a4c54218be62 -r 737589bb9bb8 src/HOL/Tools/typecopy.ML
--- a/src/HOL/Tools/typecopy.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Tools/typecopy.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -30,13 +30,12 @@
   proj_def: thm
 };
 
-structure TypecopyData = TheoryDataFun
+structure TypecopyData = Theory_Data
 (
   type T = info Symtab.table;
   val empty = Symtab.empty;
-  val copy = I;
   val extend = I;
-  fun merge _ = Symtab.merge (K true);
+  fun merge data = Symtab.merge (K true) data;
 );
 
 val get_info = Symtab.lookup o TypecopyData.get;
diff -r a4c54218be62 -r 737589bb9bb8 src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOL/Tools/typedef.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -36,13 +36,12 @@
   Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
   Rep_induct: thm, Abs_induct: thm};
 
-structure TypedefData = TheoryDataFun
+structure TypedefData = Theory_Data
 (
   type T = info Symtab.table;
   val empty = Symtab.empty;
-  val copy = I;
   val extend = I;
-  fun merge _ tabs : T = Symtab.merge (K true) tabs;
+  fun merge data = Symtab.merge (K true) data;
 );
 
 val get_info = Symtab.lookup o TypedefData.get;
diff -r a4c54218be62 -r 737589bb9bb8 src/HOLCF/Tools/fixrec.ML
--- a/src/HOLCF/Tools/fixrec.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/HOLCF/Tools/fixrec.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -252,12 +252,12 @@
 (*********** monadic notation and pattern matching compilation ***********)
 (*************************************************************************)
 
-structure FixrecMatchData = TheoryDataFun (
+structure FixrecMatchData = Theory_Data
+(
   type T = string Symtab.table;
   val empty = Symtab.empty;
-  val copy = I;
   val extend = I;
-  fun merge _ = Symtab.merge (K true);
+  fun merge data = Symtab.merge (K true) data;
 );
 
 (* associate match functions with pattern constants *)
@@ -523,8 +523,7 @@
 end;
 
 val setup =
-  FixrecMatchData.init
-  #> Attrib.setup @{binding fixrec_simp}
+  Attrib.setup @{binding fixrec_simp}
                      (Attrib.add_del fixrec_simp_add fixrec_simp_del)
                      "declaration of fixrec simp rule"
   #> Method.setup @{binding fixrec_simp}
diff -r a4c54218be62 -r 737589bb9bb8 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Provers/classical.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -835,13 +835,12 @@
 
 (* global clasets *)
 
-structure GlobalClaset = TheoryDataFun
+structure GlobalClaset = Theory_Data
 (
   type T = claset * context_cs;
   val empty = (empty_cs, empty_context_cs);
-  val copy = I;
   val extend = I;
-  fun merge _ ((cs1, ctxt_cs1), (cs2, ctxt_cs2)) =
+  fun merge ((cs1, ctxt_cs1), (cs2, ctxt_cs2)) =
     (merge_cs (cs1, cs2), merge_context_cs (ctxt_cs1, ctxt_cs2));
 );
 
diff -r a4c54218be62 -r 737589bb9bb8 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Pure/Isar/attrib.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -65,13 +65,12 @@
 
 (* theory data *)
 
-structure Attributes = TheoryDataFun
+structure Attributes = Theory_Data
 (
   type T = ((src -> attribute) * string) Name_Space.table;
   val empty : T = Name_Space.empty_table "attribute";
-  val copy = I;
   val extend = I;
-  fun merge _ tables : T = Name_Space.merge_tables tables;
+  fun merge data : T = Name_Space.merge_tables data;
 );
 
 fun print_attributes thy =
@@ -321,13 +320,12 @@
 
 (* naming *)
 
-structure Configs = TheoryDataFun
+structure Configs = Theory_Data
 (
   type T = Config.value Config.T Symtab.table;
   val empty = Symtab.empty;
-  val copy = I;
   val extend = I;
-  fun merge _ = Symtab.merge (K true);
+  fun merge data = Symtab.merge (K true) data;
 );
 
 fun print_configs ctxt =
diff -r a4c54218be62 -r 737589bb9bb8 src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Pure/Isar/class_target.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -105,13 +105,12 @@
     (Thm.merge_thms (defs1, defs2),
       AList.merge (op =) (K true) (operations1, operations2)));
 
-structure ClassData = TheoryDataFun
+structure ClassData = Theory_Data
 (
   type T = class_data Graph.T
   val empty = Graph.empty;
-  val copy = I;
   val extend = I;
-  fun merge _ = Graph.join merge_class_data;
+  val merge = Graph.join merge_class_data;
 );
 
 
diff -r a4c54218be62 -r 737589bb9bb8 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Pure/Isar/code.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -703,13 +703,12 @@
 
 (* c.f. src/HOL/Tools/recfun_codegen.ML *)
 
-structure Code_Target_Attr = TheoryDataFun (
+structure Code_Target_Attr = Theory_Data
+(
   type T = (string -> thm -> theory -> theory) option;
   val empty = NONE;
-  val copy = I;
   val extend = I;
-  fun merge _ (NONE, f2) = f2
-    | merge _ (f1, _) = f1;
+  fun merge (f1, f2) = if is_some f1 then f1 else f2;
 );
 
 fun set_code_target_attr f = Code_Target_Attr.map (K (SOME f));
diff -r a4c54218be62 -r 737589bb9bb8 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Pure/Isar/locale.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -122,13 +122,12 @@
           merge (eq_snd op =) (notes, notes')),
             merge (eq_snd op =) (dependencies, dependencies')));
 
-structure Locales = TheoryDataFun
+structure Locales = Theory_Data
 (
   type T = locale Name_Space.table;
   val empty : T = Name_Space.empty_table "locale";
-  val copy = I;
   val extend = I;
-  fun merge _ = Name_Space.join_tables (K merge_locale);
+  val merge = Name_Space.join_tables (K merge_locale);
 );
 
 val intern = Name_Space.intern o #1 o Locales.get;
@@ -332,7 +331,7 @@
 
 (*** Registrations: interpretations in theories ***)
 
-structure Registrations = TheoryDataFun
+structure Registrations = Theory_Data
 (
   type T = ((string * (morphism * morphism)) * stamp) list *
     (* registrations, in reverse order of declaration *)
@@ -340,8 +339,7 @@
     (* alist of mixin lists, per list mixins in reverse order of declaration *)
   val empty = ([], []);
   val extend = I;
-  val copy = I;
-  fun merge _ ((r1, m1), (r2, m2)) : T =
+  fun merge ((r1, m1), (r2, m2)) : T =
     (Library.merge (eq_snd op =) (r1, r2),
       AList.join (op =) (K (Library.merge (eq_snd op =))) (m1, m2));
     (* FIXME consolidate with dependencies, consider one data slot only *)
diff -r a4c54218be62 -r 737589bb9bb8 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Pure/Isar/method.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -320,13 +320,12 @@
 
 (* method definitions *)
 
-structure Methods = TheoryDataFun
+structure Methods = Theory_Data
 (
   type T = ((src -> Proof.context -> method) * string) Name_Space.table;
   val empty : T = Name_Space.empty_table "method";
-  val copy = I;
   val extend = I;
-  fun merge _ tables : T = Name_Space.merge_tables tables;
+  fun merge data : T = Name_Space.merge_tables data;
 );
 
 fun print_methods thy =
diff -r a4c54218be62 -r 737589bb9bb8 src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Pure/Isar/object_logic.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -47,18 +47,17 @@
 fun make_data (base_sort, judgment, atomize_rulify) =
   Data {base_sort = base_sort, judgment = judgment, atomize_rulify = atomize_rulify};
 
-structure ObjectLogicData = TheoryDataFun
+structure ObjectLogicData = Theory_Data
 (
   type T = data;
   val empty = make_data (NONE, NONE, ([], []));
-  val copy = I;
   val extend = I;
 
   fun merge_opt eq (SOME x, SOME y) =
         if eq (x, y) then SOME x else error "Attempt to merge different object-logics"
     | merge_opt _ (x, y) = if is_some x then x else y;
 
-  fun merge _
+  fun merge
      (Data {base_sort = base_sort1, judgment = judgment1, atomize_rulify = (atomize1, rulify1)},
       Data {base_sort = base_sort2, judgment = judgment2, atomize_rulify = (atomize2, rulify2)}) =
     make_data (merge_opt (op =) (base_sort1, base_sort2), merge_opt (op =) (judgment1, judgment2),
diff -r a4c54218be62 -r 737589bb9bb8 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Pure/Proof/extraction.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -167,7 +167,7 @@
 
 (* theory data *)
 
-structure ExtractionData = TheoryDataFun
+structure ExtractionData = Theory_Data
 (
   type T =
     {realizes_eqns : rules,
@@ -187,20 +187,19 @@
      defs = [],
      expand = [],
      prep = NONE};
-  val copy = I;
   val extend = I;
 
-  fun merge _
-    (({realizes_eqns = realizes_eqns1, typeof_eqns = typeof_eqns1, types = types1,
+  fun merge
+    ({realizes_eqns = realizes_eqns1, typeof_eqns = typeof_eqns1, types = types1,
        realizers = realizers1, defs = defs1, expand = expand1, prep = prep1},
       {realizes_eqns = realizes_eqns2, typeof_eqns = typeof_eqns2, types = types2,
-       realizers = realizers2, defs = defs2, expand = expand2, prep = prep2}) : T * T) =
+       realizers = realizers2, defs = defs2, expand = expand2, prep = prep2}) : T =
     {realizes_eqns = merge_rules realizes_eqns1 realizes_eqns2,
      typeof_eqns = merge_rules typeof_eqns1 typeof_eqns2,
      types = AList.merge (op =) (K true) (types1, types2),
      realizers = Symtab.merge_list (eq_set (op =) o pairself #1) (realizers1, realizers2),
      defs = Library.merge Thm.eq_thm (defs1, defs2),
-     expand = Library.merge (op =) (expand1, expand2),
+     expand = Library.merge (op =) (expand1, expand2),   (* FIXME proper aconv !?! *)
      prep = (case prep1 of NONE => prep2 | _ => prep1)};
 );
 
diff -r a4c54218be62 -r 737589bb9bb8 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Pure/Thy/present.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -64,13 +64,12 @@
 
 (** additional theory data **)
 
-structure BrowserInfoData = TheoryDataFun
+structure BrowserInfoData = Theory_Data
 (
   type T = {name: string, session: string list, is_local: bool};
   val empty = {name = "", session = [], is_local = false}: T;
-  val copy = I;
   fun extend _ = empty;
-  fun merge _ _ = empty;
+  fun merge _ = empty;
 );
 
 val put_info = BrowserInfoData.put;
diff -r a4c54218be62 -r 737589bb9bb8 src/Pure/Thy/term_style.ML
--- a/src/Pure/Thy/term_style.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Pure/Thy/term_style.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -19,13 +19,12 @@
 fun err_dup_style name =
   error ("Duplicate declaration of antiquote style: " ^ quote name);
 
-structure StyleData = TheoryDataFun
+structure StyleData = Theory_Data
 (
   type T = ((Proof.context -> term -> term) parser * stamp) Symtab.table;
   val empty = Symtab.empty;
-  val copy = I;
   val extend = I;
-  fun merge _ tabs : T = Symtab.merge (eq_snd (op =)) tabs
+  fun merge data : T = Symtab.merge (eq_snd (op =)) data
     handle Symtab.DUP dup => err_dup_style dup;
 );
 
diff -r a4c54218be62 -r 737589bb9bb8 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Pure/Thy/thy_info.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -233,15 +233,14 @@
 
 (* management data *)
 
-structure Management_Data = TheoryDataFun
+structure Management_Data = Theory_Data
 (
   type T =
     Task_Queue.group option *   (*worker thread group*)
     int;                        (*abstract update time*)
   val empty = (NONE, 0);
-  val copy = I;
   fun extend _ = empty;
-  fun merge _ _ = empty;
+  fun merge _ = empty;
 );
 
 val thy_ord = int_ord o pairself (#2 o Management_Data.get);
diff -r a4c54218be62 -r 737589bb9bb8 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Pure/codegen.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -185,7 +185,7 @@
 
 (* theory data *)
 
-structure CodegenData = TheoryDataFun
+structure CodegenData = Theory_Data
 (
   type T =
     {codegens : (string * term codegen) list,
@@ -198,16 +198,15 @@
   val empty =
     {codegens = [], tycodegens = [], consts = [], types = [],
      preprocs = [], modules = Symtab.empty};
-  val copy = I;
   val extend = I;
 
-  fun merge _
+  fun merge
     ({codegens = codegens1, tycodegens = tycodegens1,
       consts = consts1, types = types1,
       preprocs = preprocs1, modules = modules1} : T,
      {codegens = codegens2, tycodegens = tycodegens2,
       consts = consts2, types = types2,
-      preprocs = preprocs2, modules = modules2}) =
+      preprocs = preprocs2, modules = modules2}) : T =
     {codegens = AList.merge (op =) (K true) (codegens1, codegens2),
      tycodegens = AList.merge (op =) (K true) (tycodegens1, tycodegens2),
      consts = AList.merge (op =) (K true) (consts1, consts2),
@@ -287,13 +286,12 @@
     | _ => err ()
   end;
 
-structure UnfoldData = TheoryDataFun
+structure UnfoldData = Theory_Data
 (
   type T = simpset;
   val empty = empty_ss;
-  val copy = I;
   val extend = I;
-  fun merge _ = merge_ss;
+  val merge = merge_ss;
 );
 
 val map_unfold = UnfoldData.map;
diff -r a4c54218be62 -r 737589bb9bb8 src/Pure/interpretation.ML
--- a/src/Pure/interpretation.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Pure/interpretation.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -18,13 +18,12 @@
 
 type T = T;
 
-structure Interp = TheoryDataFun
+structure Interp = Theory_Data
 (
   type T = T list * (((T -> theory -> theory) * stamp) * T list) list;
   val empty = ([], []);
   val extend = I;
-  val copy = I;
-  fun merge _ ((data1, interps1), (data2, interps2)) : T =
+  fun merge ((data1, interps1), (data2, interps2)) : T =
     (Library.merge eq (data1, data2),
      AList.join (eq_snd (op =)) (K (Library.merge eq)) (interps1, interps2));
 );
diff -r a4c54218be62 -r 737589bb9bb8 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Pure/proofterm.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -1247,14 +1247,13 @@
 
 (**** theory data ****)
 
-structure ProofData = TheoryDataFun
+structure ProofData = Theory_Data
 (
   type T = (stamp * (proof * proof)) list * (stamp * (typ list -> proof -> proof option)) list;
 
   val empty = ([], []);
-  val copy = I;
   val extend = I;
-  fun merge _ ((rules1, procs1), (rules2, procs2)) : T =
+  fun merge ((rules1, procs1), (rules2, procs2)) : T =
     (AList.merge (op =) (K true) (rules1, rules2),
       AList.merge (op =) (K true) (procs1, procs2));
 );
diff -r a4c54218be62 -r 737589bb9bb8 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Pure/pure_thy.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -54,13 +54,12 @@
 
 (** theory data **)
 
-structure FactsData = TheoryDataFun
+structure FactsData = Theory_Data
 (
   type T = Facts.T * thm list;
   val empty = (Facts.empty, []);
-  val copy = I;
   fun extend (facts, _) = (facts, []);
-  fun merge _ ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), []);
+  fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), []);
 );
 
 
@@ -246,13 +245,12 @@
   ("_applC", typ "('b => 'a) => cargs => logic", Mixfix ("(1_/ _)", [1000, 1000], 999)),
   ("_applC", typ "('b => 'a) => cargs => aprop", Mixfix ("(1_/ _)", [1000, 1000], 999))];
 
-structure OldApplSyntax = TheoryDataFun
+structure OldApplSyntax = Theory_Data
 (
   type T = bool;
   val empty = false;
-  val copy = I;
   val extend = I;
-  fun merge _ (b1, b2) : T =
+  fun merge (b1, b2) : T =
     if b1 = b2 then b1
     else error "Cannot merge theories with different application syntax";
 );
@@ -269,7 +267,7 @@
 
 val _ = Context.>> (Context.map_theory
   (Sign.map_naming (Name_Space.set_theory_name Context.PureN) #>
-   OldApplSyntax.init #>
+   OldApplSyntax.put false #>
    Sign.add_types
    [(Binding.name "fun", 2, NoSyn),
     (Binding.name "prop", 0, NoSyn),
diff -r a4c54218be62 -r 737589bb9bb8 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Pure/thm.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -1724,13 +1724,12 @@
 
 (* authentic derivation names *)
 
-structure Oracles = TheoryDataFun
+structure Oracles = Theory_Data
 (
   type T = unit Name_Space.table;
   val empty : T = Name_Space.empty_table "oracle";
-  val copy = I;
   val extend = I;
-  fun merge _ oracles : T = Name_Space.merge_tables oracles;
+  fun merge data : T = Name_Space.merge_tables data;
 );
 
 val extern_oracles = map #1 o Name_Space.extern_table o Oracles.get;
diff -r a4c54218be62 -r 737589bb9bb8 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Tools/Code/code_preproc.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -56,13 +56,12 @@
       val functrans = AList.merge (op =) (eq_fst (op =)) (functrans1, functrans2);
     in make_thmproc ((pre, post), functrans) end;
 
-structure Code_Preproc_Data = TheoryDataFun
+structure Code_Preproc_Data = Theory_Data
 (
   type T = thmproc;
   val empty = make_thmproc ((Simplifier.empty_ss, Simplifier.empty_ss), []);
-  fun copy spec = spec;
-  val extend = copy;
-  fun merge _ = merge_thmproc;
+  val extend = I;
+  val merge = merge_thmproc;
 );
 
 fun the_thmproc thy = case Code_Preproc_Data.get thy
diff -r a4c54218be62 -r 737589bb9bb8 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Tools/Code/code_target.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -148,13 +148,12 @@
   else
     error ("Incompatible serializers: " ^ quote target);
 
-structure CodeTargetData = TheoryDataFun
+structure CodeTargetData = Theory_Data
 (
   type T = target Symtab.table * string list;
   val empty = (Symtab.empty, []);
-  val copy = I;
   val extend = I;
-  fun merge _ ((target1, exc1) : T, (target2, exc2)) =
+  fun merge ((target1, exc1), (target2, exc2)) : T =
     (Symtab.join (merge_target true) (target1, target2), Library.merge (op =) (exc1, exc2));
 );
 
diff -r a4c54218be62 -r 737589bb9bb8 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Tools/nbe.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -37,13 +37,12 @@
 
 (** certificates and oracle for "trivial type classes" **)
 
-structure Triv_Class_Data = TheoryDataFun
+structure Triv_Class_Data = Theory_Data
 (
   type T = (class * thm) list;
   val empty = [];
-  val copy = I;
   val extend = I;
-  fun merge pp = AList.merge (op =) (K true);
+  fun merge data : T = AList.merge (op =) (K true) data;
 );
 
 fun add_const_alias thm thy =
diff -r a4c54218be62 -r 737589bb9bb8 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Tools/quickcheck.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -52,16 +52,16 @@
   make_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)),
     case default_type1 of NONE => default_type2 | _ => default_type1);
 
-structure Data = TheoryDataFun(
+structure Data = Theory_Data
+(
   type T = (string * (Proof.context -> term -> int -> term list option)) list
     * test_params;
   val empty = ([], Test_Params { size = 10, iterations = 100, default_type = NONE });
-  val copy = I;
   val extend = I;
-  fun merge pp ((generators1, params1), (generators2, params2)) =
-    (AList.merge (op = : string * string -> bool) (K true) (generators1, generators2),
+  fun merge ((generators1, params1), (generators2, params2)) : T =
+    (AList.merge (op =) (K true) (generators1, generators2),
       merge_test_params (params1, params2));
-)
+);
 
 val add_generator = Data.map o apfst o AList.update (op =);
 
diff -r a4c54218be62 -r 737589bb9bb8 src/Tools/value.ML
--- a/src/Tools/value.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/Tools/value.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -15,12 +15,12 @@
 structure Value : VALUE =
 struct
 
-structure Evaluator = TheoryDataFun(
+structure Evaluator = Theory_Data
+(
   type T = (string * (Proof.context -> term -> term)) list;
   val empty = [];
-  val copy = I;
   val extend = I;
-  fun merge _ data = AList.merge (op =) (K true) data;
+  fun merge data : T = AList.merge (op =) (K true) data;
 )
 
 val add_evaluator = Evaluator.map o AList.update (op =);
diff -r a4c54218be62 -r 737589bb9bb8 src/ZF/Tools/ind_cases.ML
--- a/src/ZF/Tools/ind_cases.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/ZF/Tools/ind_cases.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -18,13 +18,12 @@
 
 (* theory data *)
 
-structure IndCasesData = TheoryDataFun
+structure IndCasesData = Theory_Data
 (
   type T = (simpset -> cterm -> thm) Symtab.table;
   val empty = Symtab.empty;
-  val copy = I;
   val extend = I;
-  fun merge _ tabs : T = Symtab.merge (K true) tabs;
+  fun merge data = Symtab.merge (K true) data;
 );
 
 
diff -r a4c54218be62 -r 737589bb9bb8 src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Sun Nov 08 18:43:22 2009 +0100
+++ b/src/ZF/Tools/induct_tacs.ML	Sun Nov 08 18:43:42 2009 +0100
@@ -29,13 +29,12 @@
    mutual_induct : thm,
    exhaustion : thm};
 
-structure DatatypesData = TheoryDataFun
+structure DatatypesData = Theory_Data
 (
   type T = datatype_info Symtab.table;
   val empty = Symtab.empty;
-  val copy = I;
   val extend = I;
-  fun merge _ tabs : T = Symtab.merge (K true) tabs;
+  fun merge data : T = Symtab.merge (K true) data;
 );
 
 
@@ -49,13 +48,12 @@
    rec_rewrites : thm list};  (*recursor equations*)
 
 
-structure ConstructorsData = TheoryDataFun
+structure ConstructorsData = Theory_Data
 (
   type T = constructor_info Symtab.table
   val empty = Symtab.empty
-  val copy = I;
   val extend = I
-  fun merge _ tabs : T = Symtab.merge (K true) tabs;
+  fun merge data = Symtab.merge (K true) data;
 );
 
 structure DatatypeTactics : DATATYPE_TACTICS =