adapted Theory_Data;
authorwenzelm
Sun Nov 08 18:43:42 2009 +0100 (2009-11-08)
changeset 33522737589bb9bb8
parent 33521 a4c54218be62
child 33523 96730ad673be
adapted Theory_Data;
tuned;
src/HOL/Boogie/Tools/boogie_split.ML
src/HOL/Boogie/Tools/boogie_vcs.ML
src/HOL/Import/hol4rews.ML
src/HOL/Import/import.ML
src/HOL/Import/shuffler.ML
src/HOL/Mirabelle/Tools/mirabelle.ML
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Tools/ATP_Manager/atp_manager.ML
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Function/scnp_reconstruct.ML
src/HOL/Tools/Function/size.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_isar.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
src/HOL/Tools/arith_data.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/recdef.ML
src/HOL/Tools/recfun_codegen.ML
src/HOL/Tools/record.ML
src/HOL/Tools/refute.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/typecopy.ML
src/HOL/Tools/typedef.ML
src/HOLCF/Tools/fixrec.ML
src/Provers/classical.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/class_target.ML
src/Pure/Isar/code.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/method.ML
src/Pure/Isar/object_logic.ML
src/Pure/Proof/extraction.ML
src/Pure/Thy/present.ML
src/Pure/Thy/term_style.ML
src/Pure/Thy/thy_info.ML
src/Pure/codegen.ML
src/Pure/interpretation.ML
src/Pure/proofterm.ML
src/Pure/pure_thy.ML
src/Pure/thm.ML
src/Tools/Code/code_preproc.ML
src/Tools/Code/code_target.ML
src/Tools/nbe.ML
src/Tools/quickcheck.ML
src/Tools/value.ML
src/ZF/Tools/ind_cases.ML
src/ZF/Tools/induct_tacs.ML
     1.1 --- a/src/HOL/Boogie/Tools/boogie_split.ML	Sun Nov 08 18:43:22 2009 +0100
     1.2 +++ b/src/HOL/Boogie/Tools/boogie_split.ML	Sun Nov 08 18:43:42 2009 +0100
     1.3 @@ -18,13 +18,12 @@
     1.4  
     1.5  (* sub-tactics store *)
     1.6  
     1.7 -structure Sub_Tactics = TheoryDataFun
     1.8 +structure Sub_Tactics = Theory_Data
     1.9  (
    1.10    type T = (Proof.context -> int -> tactic) Symtab.table
    1.11    val empty = Symtab.empty
    1.12 -  val copy = I
    1.13    val extend = I
    1.14 -  fun merge _ = Symtab.merge (K true)
    1.15 +  fun merge data = Symtab.merge (K true) data
    1.16  )
    1.17  
    1.18  fun add_sub_tactic tac = Sub_Tactics.map (Symtab.update_new tac)
     2.1 --- a/src/HOL/Boogie/Tools/boogie_vcs.ML	Sun Nov 08 18:43:22 2009 +0100
     2.2 +++ b/src/HOL/Boogie/Tools/boogie_vcs.ML	Sun Nov 08 18:43:42 2009 +0100
     2.3 @@ -19,14 +19,13 @@
     2.4  
     2.5  fun err_vcs () = error "undischarged Boogie verification conditions found"
     2.6  
     2.7 -structure VCs = TheoryDataFun
     2.8 +structure VCs = Theory_Data
     2.9  (
    2.10 -  type T = (Term.term * bool) Symtab.table option
    2.11 +  type T = (term * bool) Symtab.table option
    2.12    val empty = NONE
    2.13 -  val copy = I
    2.14    val extend = I
    2.15 -  fun merge _ (NONE, NONE) = NONE
    2.16 -    | merge _ (_, _) = err_vcs ()
    2.17 +  fun merge (NONE, NONE) = NONE
    2.18 +    | merge _ = err_vcs ()
    2.19  )
    2.20  
    2.21  fun set vcs = VCs.map (fn
     3.1 --- a/src/HOL/Import/hol4rews.ML	Sun Nov 08 18:43:22 2009 +0100
     3.2 +++ b/src/HOL/Import/hol4rews.ML	Sun Nov 08 18:43:42 2009 +0100
     3.3 @@ -11,25 +11,23 @@
     3.4         | Generating of string
     3.5         | Replaying of string
     3.6  
     3.7 -structure HOL4DefThy = TheoryDataFun
     3.8 +structure HOL4DefThy = Theory_Data
     3.9  (
    3.10    type T = ImportStatus
    3.11    val empty = NoImport
    3.12 -  val copy = I
    3.13    val extend = I
    3.14 -  fun merge _ (NoImport,NoImport) = NoImport
    3.15 -    | merge _ _ = (warning "Import status set during merge"; NoImport)
    3.16 +  fun merge (NoImport, NoImport) = NoImport
    3.17 +    | merge _ = (warning "Import status set during merge"; NoImport)
    3.18  )
    3.19  
    3.20 -structure ImportSegment = TheoryDataFun
    3.21 +structure ImportSegment = Theory_Data
    3.22  (
    3.23    type T = string
    3.24    val empty = ""
    3.25 -  val copy = I
    3.26    val extend = I
    3.27 -  fun merge _ ("",arg) = arg
    3.28 -    | merge _ (arg,"") = arg
    3.29 -    | merge _ (s1,s2) =
    3.30 +  fun merge ("",arg) = arg
    3.31 +    | merge (arg,"") = arg
    3.32 +    | merge (s1,s2) =
    3.33        if s1 = s2
    3.34        then s1
    3.35        else error "Trying to merge two different import segments"
    3.36 @@ -38,42 +36,38 @@
    3.37  val get_import_segment = ImportSegment.get
    3.38  val set_import_segment = ImportSegment.put
    3.39  
    3.40 -structure HOL4UNames = TheoryDataFun
    3.41 +structure HOL4UNames = Theory_Data
    3.42  (
    3.43    type T = string list
    3.44    val empty = []
    3.45 -  val copy = I
    3.46    val extend = I
    3.47 -  fun merge _ ([],[]) = []
    3.48 -    | merge _ _ = error "Used names not empty during merge"
    3.49 +  fun merge ([], []) = []
    3.50 +    | merge _ = error "Used names not empty during merge"
    3.51  )
    3.52  
    3.53 -structure HOL4Dump = TheoryDataFun
    3.54 +structure HOL4Dump = Theory_Data
    3.55  (
    3.56    type T = string * string * string list
    3.57    val empty = ("","",[])
    3.58 -  val copy = I
    3.59    val extend = I
    3.60 -  fun merge _ (("","",[]),("","",[])) = ("","",[])
    3.61 -    | merge _ _ = error "Dump data not empty during merge"
    3.62 +  fun merge (("","",[]),("","",[])) = ("","",[])
    3.63 +    | merge _ = error "Dump data not empty during merge"
    3.64  )
    3.65  
    3.66 -structure HOL4Moves = TheoryDataFun
    3.67 +structure HOL4Moves = Theory_Data
    3.68  (
    3.69    type T = string Symtab.table
    3.70    val empty = Symtab.empty
    3.71 -  val copy = I
    3.72    val extend = I
    3.73 -  fun merge _ : T * T -> T = Symtab.merge (K true)
    3.74 +  fun merge data = Symtab.merge (K true) data
    3.75  )
    3.76  
    3.77 -structure HOL4Imports = TheoryDataFun
    3.78 +structure HOL4Imports = Theory_Data
    3.79  (
    3.80    type T = string Symtab.table
    3.81    val empty = Symtab.empty
    3.82 -  val copy = I
    3.83    val extend = I
    3.84 -  fun merge _ : T * T -> T = Symtab.merge (K true)
    3.85 +  fun merge data = Symtab.merge (K true) data
    3.86  )
    3.87  
    3.88  fun get_segment2 thyname thy =
    3.89 @@ -87,85 +81,76 @@
    3.90          HOL4Imports.put imps' thy
    3.91      end
    3.92  
    3.93 -structure HOL4CMoves = TheoryDataFun
    3.94 +structure HOL4CMoves = Theory_Data
    3.95  (
    3.96    type T = string Symtab.table
    3.97    val empty = Symtab.empty
    3.98 -  val copy = I
    3.99    val extend = I
   3.100 -  fun merge _ : T * T -> T = Symtab.merge (K true)
   3.101 +  fun merge data = Symtab.merge (K true) data
   3.102  )
   3.103  
   3.104 -structure HOL4Maps = TheoryDataFun
   3.105 +structure HOL4Maps = Theory_Data
   3.106  (
   3.107 -  type T = (string option) StringPair.table
   3.108 +  type T = string option StringPair.table
   3.109    val empty = StringPair.empty
   3.110 -  val copy = I
   3.111    val extend = I
   3.112 -  fun merge _ : T * T -> T = StringPair.merge (K true)
   3.113 +  fun merge data = StringPair.merge (K true) data
   3.114  )
   3.115  
   3.116 -structure HOL4Thms = TheoryDataFun
   3.117 +structure HOL4Thms = Theory_Data
   3.118  (
   3.119    type T = holthm StringPair.table
   3.120    val empty = StringPair.empty
   3.121 -  val copy = I
   3.122    val extend = I
   3.123 -  fun merge _ : T * T -> T = StringPair.merge (K true)
   3.124 +  fun merge data = StringPair.merge (K true) data
   3.125  )
   3.126  
   3.127 -structure HOL4ConstMaps = TheoryDataFun
   3.128 +structure HOL4ConstMaps = Theory_Data
   3.129  (
   3.130    type T = (bool * string * typ option) StringPair.table
   3.131    val empty = StringPair.empty
   3.132 -  val copy = I
   3.133    val extend = I
   3.134 -  fun merge _ : T * T -> T = StringPair.merge (K true)
   3.135 +  fun merge data = StringPair.merge (K true) data
   3.136  )
   3.137  
   3.138 -structure HOL4Rename = TheoryDataFun
   3.139 +structure HOL4Rename = Theory_Data
   3.140  (
   3.141    type T = string StringPair.table
   3.142    val empty = StringPair.empty
   3.143 -  val copy = I
   3.144    val extend = I
   3.145 -  fun merge _ : T * T -> T = StringPair.merge (K true)
   3.146 +  fun merge data = StringPair.merge (K true) data
   3.147  )
   3.148  
   3.149 -structure HOL4DefMaps = TheoryDataFun
   3.150 +structure HOL4DefMaps = Theory_Data
   3.151  (
   3.152    type T = string StringPair.table
   3.153    val empty = StringPair.empty
   3.154 -  val copy = I
   3.155    val extend = I
   3.156 -  fun merge _ : T * T -> T = StringPair.merge (K true)
   3.157 +  fun merge data = StringPair.merge (K true) data
   3.158  )
   3.159  
   3.160 -structure HOL4TypeMaps = TheoryDataFun
   3.161 +structure HOL4TypeMaps = Theory_Data
   3.162  (
   3.163    type T = (bool * string) StringPair.table
   3.164    val empty = StringPair.empty
   3.165 -  val copy = I
   3.166    val extend = I
   3.167 -  fun merge _ : T * T -> T = StringPair.merge (K true)
   3.168 +  fun merge data = StringPair.merge (K true) data
   3.169  )
   3.170  
   3.171 -structure HOL4Pending = TheoryDataFun
   3.172 +structure HOL4Pending = Theory_Data
   3.173  (
   3.174    type T = ((term * term) list * thm) StringPair.table
   3.175    val empty = StringPair.empty
   3.176 -  val copy = I
   3.177    val extend = I
   3.178 -  fun merge _ : T * T -> T = StringPair.merge (K true)
   3.179 +  fun merge data = StringPair.merge (K true) data
   3.180  )
   3.181  
   3.182 -structure HOL4Rewrites = TheoryDataFun
   3.183 +structure HOL4Rewrites = Theory_Data
   3.184  (
   3.185    type T = thm list
   3.186    val empty = []
   3.187 -  val copy = I
   3.188    val extend = I
   3.189 -  fun merge _ = Library.merge Thm.eq_thm_prop
   3.190 +  val merge = Thm.merge_thms
   3.191  )
   3.192  
   3.193  val hol4_debug = Unsynchronized.ref false
     4.1 --- a/src/HOL/Import/import.ML	Sun Nov 08 18:43:22 2009 +0100
     4.2 +++ b/src/HOL/Import/import.ML	Sun Nov 08 18:43:42 2009 +0100
     4.3 @@ -9,13 +9,12 @@
     4.4      val setup      : theory -> theory
     4.5  end
     4.6  
     4.7 -structure ImportData = TheoryDataFun
     4.8 +structure ImportData = Theory_Data
     4.9  (
    4.10 -  type T = ProofKernel.thm option array option
    4.11 +  type T = ProofKernel.thm option array option  (* FIXME mutable array !??!!! *)
    4.12    val empty = NONE
    4.13 -  val copy = I
    4.14    val extend = I
    4.15 -  fun merge _ _ = NONE
    4.16 +  fun merge _ = NONE
    4.17  )
    4.18  
    4.19  structure Import :> IMPORT =
     5.1 --- a/src/HOL/Import/shuffler.ML	Sun Nov 08 18:43:22 2009 +0100
     5.2 +++ b/src/HOL/Import/shuffler.ML	Sun Nov 08 18:43:42 2009 +0100
     5.3 @@ -72,13 +72,12 @@
     5.4         | _ => raise THM("Not an equality",0,[th]))
     5.5      handle _ => raise THM("Couldn't make object equality",0,[th])  (* FIXME avoid handle _ *)
     5.6  
     5.7 -structure ShuffleData = TheoryDataFun
     5.8 +structure ShuffleData = Theory_Data
     5.9  (
    5.10    type T = thm list
    5.11    val empty = []
    5.12 -  val copy = I
    5.13    val extend = I
    5.14 -  fun merge _ = Library.merge Thm.eq_thm_prop
    5.15 +  val merge = Thm.merge_thms
    5.16  )
    5.17  
    5.18  fun print_shuffles thy =
     6.1 --- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Sun Nov 08 18:43:22 2009 +0100
     6.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Sun Nov 08 18:43:42 2009 +0100
     6.3 @@ -60,13 +60,12 @@
     6.4  type run_action = int -> run_args -> unit
     6.5  type action = init_action * run_action * done_action
     6.6  
     6.7 -structure Actions = TheoryDataFun
     6.8 +structure Actions = Theory_Data
     6.9  (
    6.10    type T = (int * run_action * done_action) list
    6.11    val empty = []
    6.12 -  val copy = I
    6.13    val extend = I
    6.14 -  fun merge _ = Library.merge (K true)
    6.15 +  fun merge data = Library.merge (K true) data  (* FIXME ?!? *)
    6.16  )
    6.17  
    6.18  
     7.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Sun Nov 08 18:43:22 2009 +0100
     7.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Sun Nov 08 18:43:42 2009 +0100
     7.3 @@ -42,13 +42,12 @@
     7.4     cp_inst : thm Symtab.table,
     7.5     dj_thms : thm Symtab.table};
     7.6  
     7.7 -structure NominalData = TheoryDataFun
     7.8 +structure NominalData = Theory_Data
     7.9  (
    7.10    type T = atom_info Symtab.table;
    7.11    val empty = Symtab.empty;
    7.12 -  val copy = I;
    7.13    val extend = I;
    7.14 -  fun merge _ x = Symtab.merge (K true) x;
    7.15 +  fun merge data = Symtab.merge (K true) data;
    7.16  );
    7.17  
    7.18  fun make_atom_info ((((((pt_class, fs_class), cp_classes), at_inst), pt_inst), cp_inst), dj_thms) =
     8.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Sun Nov 08 18:43:22 2009 +0100
     8.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Sun Nov 08 18:43:42 2009 +0100
     8.3 @@ -84,13 +84,12 @@
     8.4     distinct : thm list,
     8.5     inject : thm list};
     8.6  
     8.7 -structure NominalDatatypesData = TheoryDataFun
     8.8 +structure NominalDatatypesData = Theory_Data
     8.9  (
    8.10    type T = nominal_datatype_info Symtab.table;
    8.11    val empty = Symtab.empty;
    8.12 -  val copy = I;
    8.13    val extend = I;
    8.14 -  fun merge _ tabs : T = Symtab.merge (K true) tabs;
    8.15 +  fun merge data = Symtab.merge (K true) data;
    8.16  );
    8.17  
    8.18  val get_nominal_datatypes = NominalDatatypesData.get;
     9.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Sun Nov 08 18:43:22 2009 +0100
     9.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Sun Nov 08 18:43:42 2009 +0100
     9.3 @@ -226,13 +226,12 @@
     9.4  
     9.5  fun err_dup_prover name = error ("Duplicate prover: " ^ quote name);
     9.6  
     9.7 -structure Provers = TheoryDataFun
     9.8 +structure Provers = Theory_Data
     9.9  (
    9.10    type T = (ATP_Wrapper.prover * stamp) Symtab.table;
    9.11    val empty = Symtab.empty;
    9.12 -  val copy = I;
    9.13    val extend = I;
    9.14 -  fun merge _ tabs : T = Symtab.merge (eq_snd op =) tabs
    9.15 +  fun merge data : T = Symtab.merge (eq_snd op =) data
    9.16      handle Symtab.DUP dup => err_dup_prover dup;
    9.17  );
    9.18  
    10.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Sun Nov 08 18:43:22 2009 +0100
    10.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Sun Nov 08 18:43:42 2009 +0100
    10.3 @@ -42,7 +42,7 @@
    10.4  
    10.5  (* data management *)
    10.6  
    10.7 -structure DatatypesData = TheoryDataFun
    10.8 +structure DatatypesData = Theory_Data
    10.9  (
   10.10    type T =
   10.11      {types: info Symtab.table,
   10.12 @@ -51,11 +51,10 @@
   10.13  
   10.14    val empty =
   10.15      {types = Symtab.empty, constrs = Symtab.empty, cases = Symtab.empty};
   10.16 -  val copy = I;
   10.17    val extend = I;
   10.18 -  fun merge _
   10.19 +  fun merge
   10.20      ({types = types1, constrs = constrs1, cases = cases1},
   10.21 -     {types = types2, constrs = constrs2, cases = cases2}) =
   10.22 +     {types = types2, constrs = constrs2, cases = cases2}) : T =
   10.23      {types = Symtab.merge (K true) (types1, types2),
   10.24       constrs = Symtab.join (K (AList.merge (op =) (K true))) (constrs1, constrs2),
   10.25       cases = Symtab.merge (K true) (cases1, cases2)};
    11.1 --- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Sun Nov 08 18:43:22 2009 +0100
    11.2 +++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Sun Nov 08 18:43:42 2009 +0100
    11.3 @@ -63,13 +63,12 @@
    11.4     reduction_pair : thm
    11.5    }
    11.6  
    11.7 -structure Multiset_Setup = TheoryDataFun
    11.8 +structure Multiset_Setup = Theory_Data
    11.9  (
   11.10    type T = multiset_setup option
   11.11    val empty = NONE
   11.12 -  val copy = I;
   11.13    val extend = I;
   11.14 -  fun merge _ (v1, v2) = if is_some v2 then v2 else v1
   11.15 +  fun merge (v1, v2) = if is_some v2 then v2 else v1   (* FIXME prefer v1 !?! *)
   11.16  )
   11.17  
   11.18  val multiset_setup = Multiset_Setup.put o SOME
    12.1 --- a/src/HOL/Tools/Function/size.ML	Sun Nov 08 18:43:22 2009 +0100
    12.2 +++ b/src/HOL/Tools/Function/size.ML	Sun Nov 08 18:43:42 2009 +0100
    12.3 @@ -15,13 +15,12 @@
    12.4  
    12.5  open DatatypeAux;
    12.6  
    12.7 -structure SizeData = TheoryDataFun
    12.8 +structure SizeData = Theory_Data
    12.9  (
   12.10    type T = (string * thm list) Symtab.table;
   12.11    val empty = Symtab.empty;
   12.12 -  val copy = I
   12.13    val extend = I
   12.14 -  fun merge _ = Symtab.merge (K true);
   12.15 +  fun merge data = Symtab.merge (K true) data;
   12.16  );
   12.17  
   12.18  val lookup_size = SizeData.get #> Symtab.lookup;
    13.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Nov 08 18:43:22 2009 +0100
    13.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Nov 08 18:43:42 2009 +0100
    13.3 @@ -179,14 +179,13 @@
    13.4    unrolled_preds: unrolled list Unsynchronized.ref,
    13.5    wf_cache: wf_cache Unsynchronized.ref}
    13.6  
    13.7 -structure TheoryData = TheoryDataFun(
    13.8 +structure TheoryData = Theory_Data(
    13.9    type T = {frac_types: (string * (string * string) list) list,
   13.10              codatatypes: (string * (string * styp list)) list}
   13.11    val empty = {frac_types = [], codatatypes = []}
   13.12 -  val copy = I
   13.13    val extend = I
   13.14 -  fun merge _ ({frac_types = fs1, codatatypes = cs1},
   13.15 -               {frac_types = fs2, codatatypes = cs2}) =
   13.16 +  fun merge ({frac_types = fs1, codatatypes = cs1},
   13.17 +               {frac_types = fs2, codatatypes = cs2}) : T =
   13.18      {frac_types = AList.merge (op =) (op =) (fs1, fs2),
   13.19       codatatypes = AList.merge (op =) (op =) (cs1, cs2)})
   13.20  
    14.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sun Nov 08 18:43:22 2009 +0100
    14.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Sun Nov 08 18:43:42 2009 +0100
    14.3 @@ -125,13 +125,12 @@
    14.4                            | _ => value)
    14.5    | NONE => (name, value)
    14.6  
    14.7 -structure TheoryData = TheoryDataFun(
    14.8 +structure TheoryData = Theory_Data(
    14.9    type T = {params: raw_param list, registered_auto: bool}
   14.10    val empty = {params = rev default_default_params, registered_auto = false}
   14.11 -  val copy = I
   14.12    val extend = I
   14.13 -  fun merge _ ({params = ps1, registered_auto = a1},
   14.14 -               {params = ps2, registered_auto = a2}) =
   14.15 +  fun merge ({params = ps1, registered_auto = a1},
   14.16 +               {params = ps2, registered_auto = a2}) : T =
   14.17      {params = AList.merge (op =) (op =) (ps1, ps2),
   14.18       registered_auto = a1 orelse a2})
   14.19  
    15.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Nov 08 18:43:22 2009 +0100
    15.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Nov 08 18:43:42 2009 +0100
    15.3 @@ -232,13 +232,12 @@
    15.4    eq_option (Thm.eq_thm) (#elim d1, #elim d2) andalso
    15.5    #nparams d1 = #nparams d2
    15.6  
    15.7 -structure PredData = TheoryDataFun
    15.8 +structure PredData = Theory_Data
    15.9  (
   15.10    type T = pred_data Graph.T;
   15.11    val empty = Graph.empty;
   15.12 -  val copy = I;
   15.13    val extend = I;
   15.14 -  fun merge _ = Graph.merge eq_pred_data;
   15.15 +  val merge = Graph.merge eq_pred_data;
   15.16  );
   15.17  
   15.18  (* queries *)
   15.19 @@ -2450,7 +2449,7 @@
   15.20    (*FIXME name discrepancy in attribs and ML code*)
   15.21    (*FIXME intros should be better named intro*)
   15.22  
   15.23 -(* TODO: make TheoryDataFun to Generic_Data & remove duplication of local theory and theory *)
   15.24 +(* TODO: make Theory_Data to Generic_Data & remove duplication of local theory and theory *)
   15.25  fun generic_code_pred prep_const options raw_const lthy =
   15.26    let
   15.27      val thy = ProofContext.theory_of lthy
    16.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Sun Nov 08 18:43:22 2009 +0100
    16.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Sun Nov 08 18:43:42 2009 +0100
    16.3 @@ -19,15 +19,14 @@
    16.4  
    16.5  open Predicate_Compile_Aux;
    16.6  
    16.7 -structure Data = TheoryDataFun
    16.8 +structure Data = Theory_Data
    16.9  (
   16.10    type T =
   16.11      {const_spec_table : thm list Symtab.table};
   16.12    val empty =
   16.13      {const_spec_table = Symtab.empty};
   16.14 -  val copy = I;
   16.15    val extend = I;
   16.16 -  fun merge _
   16.17 +  fun merge
   16.18      ({const_spec_table = const_spec_table1},
   16.19       {const_spec_table = const_spec_table2}) =
   16.20       {const_spec_table = Symtab.merge (K true) (const_spec_table1, const_spec_table2)}
    17.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Sun Nov 08 18:43:22 2009 +0100
    17.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Sun Nov 08 18:43:42 2009 +0100
    17.3 @@ -56,13 +56,12 @@
    17.4  fun is_constr thy = is_some o Code.get_datatype_of_constr thy;
    17.5  
    17.6  (* Table from constant name (string) to term of inductive predicate *)
    17.7 -structure Pred_Compile_Preproc = TheoryDataFun
    17.8 +structure Pred_Compile_Preproc = Theory_Data
    17.9  (
   17.10    type T = string Symtab.table;
   17.11    val empty = Symtab.empty;
   17.12 -  val copy = I;
   17.13    val extend = I;
   17.14 -  fun merge _ = Symtab.merge (op =);
   17.15 +  fun merge data : T = Symtab.merge (op =) data;   (* FIXME handle Symtab.DUP ?? *)
   17.16  )
   17.17  
   17.18  fun pred_of_function thy name = Symtab.lookup (Pred_Compile_Preproc.get thy) name
    18.1 --- a/src/HOL/Tools/arith_data.ML	Sun Nov 08 18:43:22 2009 +0100
    18.2 +++ b/src/HOL/Tools/arith_data.ML	Sun Nov 08 18:43:42 2009 +0100
    18.3 @@ -41,13 +41,12 @@
    18.4  
    18.5  val get_arith_facts = Arith_Facts.get;
    18.6  
    18.7 -structure Arith_Tactics = TheoryDataFun
    18.8 +structure Arith_Tactics = Theory_Data
    18.9  (
   18.10    type T = (serial * (string * (bool -> Proof.context -> int -> tactic))) list;
   18.11    val empty = [];
   18.12 -  val copy = I;
   18.13    val extend = I;
   18.14 -  fun merge _ = AList.merge (op =) (K true);
   18.15 +  fun merge data : T = AList.merge (op =) (K true) data;
   18.16  );
   18.17  
   18.18  fun add_tactic name tac = Arith_Tactics.map (cons (serial (), (name, tac)));
    19.1 --- a/src/HOL/Tools/inductive_codegen.ML	Sun Nov 08 18:43:22 2009 +0100
    19.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Sun Nov 08 18:43:42 2009 +0100
    19.3 @@ -20,7 +20,7 @@
    19.4  fun merge_rules tabs =
    19.5    Symtab.join (fn _ => AList.merge (Thm.eq_thm_prop) (K true)) tabs;
    19.6  
    19.7 -structure CodegenData = TheoryDataFun
    19.8 +structure CodegenData = Theory_Data
    19.9  (
   19.10    type T =
   19.11      {intros : (thm * (string * int)) list Symtab.table,
   19.12 @@ -28,10 +28,9 @@
   19.13       eqns : (thm * string) list Symtab.table};
   19.14    val empty =
   19.15      {intros = Symtab.empty, graph = Graph.empty, eqns = Symtab.empty};
   19.16 -  val copy = I;
   19.17    val extend = I;
   19.18 -  fun merge _ ({intros=intros1, graph=graph1, eqns=eqns1},
   19.19 -    {intros=intros2, graph=graph2, eqns=eqns2}) =
   19.20 +  fun merge ({intros=intros1, graph=graph1, eqns=eqns1},
   19.21 +    {intros=intros2, graph=graph2, eqns=eqns2}) : T =
   19.22      {intros = merge_rules (intros1, intros2),
   19.23       graph = Graph.merge (K true) (graph1, graph2),
   19.24       eqns = merge_rules (eqns1, eqns2)};
    20.1 --- a/src/HOL/Tools/recdef.ML	Sun Nov 08 18:43:22 2009 +0100
    20.2 +++ b/src/HOL/Tools/recdef.ML	Sun Nov 08 18:43:42 2009 +0100
    20.3 @@ -86,18 +86,17 @@
    20.4  
    20.5  type recdef_info = {simps: thm list, rules: thm list list, induct: thm, tcs: term list};
    20.6  
    20.7 -structure GlobalRecdefData = TheoryDataFun
    20.8 +structure GlobalRecdefData = Theory_Data
    20.9  (
   20.10    type T = recdef_info Symtab.table * hints;
   20.11    val empty = (Symtab.empty, mk_hints ([], [], [])): T;
   20.12 -  val copy = I;
   20.13    val extend = I;
   20.14 -  fun merge _
   20.15 +  fun merge
   20.16     ((tab1, {simps = simps1, congs = congs1, wfs = wfs1}),
   20.17      (tab2, {simps = simps2, congs = congs2, wfs = wfs2})) : T =
   20.18        (Symtab.merge (K true) (tab1, tab2),
   20.19          mk_hints (Thm.merge_thms (simps1, simps2),
   20.20 -          AList.merge (op =) Thm.eq_thm (congs1, congs2),
   20.21 +          AList.merge (op =) Thm.eq_thm_prop (congs1, congs2),
   20.22            Thm.merge_thms (wfs1, wfs2)));
   20.23  );
   20.24  
    21.1 --- a/src/HOL/Tools/recfun_codegen.ML	Sun Nov 08 18:43:22 2009 +0100
    21.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Sun Nov 08 18:43:42 2009 +0100
    21.3 @@ -16,13 +16,12 @@
    21.4  
    21.5  val const_of = dest_Const o head_of o fst o Logic.dest_equals;
    21.6  
    21.7 -structure ModuleData = TheoryDataFun
    21.8 +structure ModuleData = Theory_Data
    21.9  (
   21.10    type T = string Symtab.table;
   21.11    val empty = Symtab.empty;
   21.12 -  val copy = I;
   21.13    val extend = I;
   21.14 -  fun merge _ = Symtab.merge (K true);
   21.15 +  fun merge data = Symtab.merge (K true) data;
   21.16  );
   21.17  
   21.18  fun add_thm_target module_name thm thy =
    22.1 --- a/src/HOL/Tools/record.ML	Sun Nov 08 18:43:22 2009 +0100
    22.2 +++ b/src/HOL/Tools/record.ML	Sun Nov 08 18:43:42 2009 +0100
    22.3 @@ -81,13 +81,12 @@
    22.4      cterm_instantiate (map (apfst getvar) values) thm
    22.5    end;
    22.6  
    22.7 -structure IsTupleThms = TheoryDataFun
    22.8 +structure IsTupleThms = Theory_Data
    22.9  (
   22.10    type T = thm Symtab.table;
   22.11    val empty = Symtab.make [tuple_istuple];
   22.12 -  val copy = I;
   22.13    val extend = I;
   22.14 -  fun merge _ = Symtab.merge Thm.eq_thm_prop;
   22.15 +  fun merge data = Symtab.merge Thm.eq_thm_prop data;   (* FIXME handle Symtab.DUP ?? *)
   22.16  );
   22.17  
   22.18  fun do_typedef name repT alphas thy =
   22.19 @@ -381,7 +380,7 @@
   22.20    equalities = equalities, extinjects=extinjects, extsplit = extsplit, splits = splits,
   22.21    extfields = extfields, fieldext = fieldext }: record_data;
   22.22  
   22.23 -structure RecordsData = TheoryDataFun
   22.24 +structure RecordsData = Theory_Data
   22.25  (
   22.26    type T = record_data;
   22.27    val empty =
   22.28 @@ -390,10 +389,8 @@
   22.29            simpset = HOL_basic_ss, defset = HOL_basic_ss,
   22.30            foldcong = HOL_basic_ss, unfoldcong = HOL_basic_ss}
   22.31         Symtab.empty [] Symtab.empty Symtab.empty Symtab.empty Symtab.empty;
   22.32 -
   22.33 -  val copy = I;
   22.34    val extend = I;
   22.35 -  fun merge _
   22.36 +  fun merge
   22.37     ({records = recs1,
   22.38       sel_upd =
   22.39        {selectors = sels1, updates = upds1,
   22.40 @@ -425,7 +422,7 @@
   22.41          foldcong = Simplifier.merge_ss (fc1, fc2),
   22.42          unfoldcong = Simplifier.merge_ss (uc1, uc2)}
   22.43        (Symtab.merge Thm.eq_thm_prop (equalities1, equalities2))
   22.44 -      (Library.merge Thm.eq_thm_prop (extinjects1, extinjects2))
   22.45 +      (Thm.merge_thms (extinjects1, extinjects2))
   22.46        (Symtab.merge Thm.eq_thm_prop (extsplit1, extsplit2))
   22.47        (Symtab.merge (fn ((a, b, c, d), (w, x, y, z)) =>
   22.48            Thm.eq_thm (a, w) andalso Thm.eq_thm (b, x) andalso
    23.1 --- a/src/HOL/Tools/refute.ML	Sun Nov 08 18:43:22 2009 +0100
    23.2 +++ b/src/HOL/Tools/refute.ML	Sun Nov 08 18:43:42 2009 +0100
    23.3 @@ -201,7 +201,7 @@
    23.4      };
    23.5  
    23.6  
    23.7 -  structure RefuteData = TheoryDataFun
    23.8 +  structure RefuteData = Theory_Data
    23.9    (
   23.10      type T =
   23.11        {interpreters: (string * (theory -> model -> arguments -> term ->
   23.12 @@ -210,11 +210,10 @@
   23.13          (int -> bool) -> term option)) list,
   23.14         parameters: string Symtab.table};
   23.15      val empty = {interpreters = [], printers = [], parameters = Symtab.empty};
   23.16 -    val copy = I;
   23.17      val extend = I;
   23.18 -    fun merge _
   23.19 +    fun merge
   23.20        ({interpreters = in1, printers = pr1, parameters = pa1},
   23.21 -       {interpreters = in2, printers = pr2, parameters = pa2}) =
   23.22 +       {interpreters = in2, printers = pr2, parameters = pa2}) : T =
   23.23        {interpreters = AList.merge (op =) (K true) (in1, in2),
   23.24         printers = AList.merge (op =) (K true) (pr1, pr2),
   23.25         parameters = Symtab.merge (op=) (pa1, pa2)};
    24.1 --- a/src/HOL/Tools/res_axioms.ML	Sun Nov 08 18:43:22 2009 +0100
    24.2 +++ b/src/HOL/Tools/res_axioms.ML	Sun Nov 08 18:43:42 2009 +0100
    24.3 @@ -349,13 +349,12 @@
    24.4  
    24.5  (*The cache prevents repeated clausification of a theorem, and also repeated declaration of
    24.6    Skolem functions.*)
    24.7 -structure ThmCache = TheoryDataFun
    24.8 +structure ThmCache = Theory_Data
    24.9  (
   24.10    type T = thm list Thmtab.table * unit Symtab.table;
   24.11    val empty = (Thmtab.empty, Symtab.empty);
   24.12 -  val copy = I;
   24.13    val extend = I;
   24.14 -  fun merge _ ((cache1, seen1), (cache2, seen2)) : T =
   24.15 +  fun merge ((cache1, seen1), (cache2, seen2)) : T =
   24.16      (Thmtab.merge (K true) (cache1, cache2), Symtab.merge (K true) (seen1, seen2));
   24.17  );
   24.18  
    25.1 --- a/src/HOL/Tools/typecopy.ML	Sun Nov 08 18:43:22 2009 +0100
    25.2 +++ b/src/HOL/Tools/typecopy.ML	Sun Nov 08 18:43:42 2009 +0100
    25.3 @@ -30,13 +30,12 @@
    25.4    proj_def: thm
    25.5  };
    25.6  
    25.7 -structure TypecopyData = TheoryDataFun
    25.8 +structure TypecopyData = Theory_Data
    25.9  (
   25.10    type T = info Symtab.table;
   25.11    val empty = Symtab.empty;
   25.12 -  val copy = I;
   25.13    val extend = I;
   25.14 -  fun merge _ = Symtab.merge (K true);
   25.15 +  fun merge data = Symtab.merge (K true) data;
   25.16  );
   25.17  
   25.18  val get_info = Symtab.lookup o TypecopyData.get;
    26.1 --- a/src/HOL/Tools/typedef.ML	Sun Nov 08 18:43:22 2009 +0100
    26.2 +++ b/src/HOL/Tools/typedef.ML	Sun Nov 08 18:43:42 2009 +0100
    26.3 @@ -36,13 +36,12 @@
    26.4    Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
    26.5    Rep_induct: thm, Abs_induct: thm};
    26.6  
    26.7 -structure TypedefData = TheoryDataFun
    26.8 +structure TypedefData = Theory_Data
    26.9  (
   26.10    type T = info Symtab.table;
   26.11    val empty = Symtab.empty;
   26.12 -  val copy = I;
   26.13    val extend = I;
   26.14 -  fun merge _ tabs : T = Symtab.merge (K true) tabs;
   26.15 +  fun merge data = Symtab.merge (K true) data;
   26.16  );
   26.17  
   26.18  val get_info = Symtab.lookup o TypedefData.get;
    27.1 --- a/src/HOLCF/Tools/fixrec.ML	Sun Nov 08 18:43:22 2009 +0100
    27.2 +++ b/src/HOLCF/Tools/fixrec.ML	Sun Nov 08 18:43:42 2009 +0100
    27.3 @@ -252,12 +252,12 @@
    27.4  (*********** monadic notation and pattern matching compilation ***********)
    27.5  (*************************************************************************)
    27.6  
    27.7 -structure FixrecMatchData = TheoryDataFun (
    27.8 +structure FixrecMatchData = Theory_Data
    27.9 +(
   27.10    type T = string Symtab.table;
   27.11    val empty = Symtab.empty;
   27.12 -  val copy = I;
   27.13    val extend = I;
   27.14 -  fun merge _ = Symtab.merge (K true);
   27.15 +  fun merge data = Symtab.merge (K true) data;
   27.16  );
   27.17  
   27.18  (* associate match functions with pattern constants *)
   27.19 @@ -523,8 +523,7 @@
   27.20  end;
   27.21  
   27.22  val setup =
   27.23 -  FixrecMatchData.init
   27.24 -  #> Attrib.setup @{binding fixrec_simp}
   27.25 +  Attrib.setup @{binding fixrec_simp}
   27.26                       (Attrib.add_del fixrec_simp_add fixrec_simp_del)
   27.27                       "declaration of fixrec simp rule"
   27.28    #> Method.setup @{binding fixrec_simp}
    28.1 --- a/src/Provers/classical.ML	Sun Nov 08 18:43:22 2009 +0100
    28.2 +++ b/src/Provers/classical.ML	Sun Nov 08 18:43:42 2009 +0100
    28.3 @@ -835,13 +835,12 @@
    28.4  
    28.5  (* global clasets *)
    28.6  
    28.7 -structure GlobalClaset = TheoryDataFun
    28.8 +structure GlobalClaset = Theory_Data
    28.9  (
   28.10    type T = claset * context_cs;
   28.11    val empty = (empty_cs, empty_context_cs);
   28.12 -  val copy = I;
   28.13    val extend = I;
   28.14 -  fun merge _ ((cs1, ctxt_cs1), (cs2, ctxt_cs2)) =
   28.15 +  fun merge ((cs1, ctxt_cs1), (cs2, ctxt_cs2)) =
   28.16      (merge_cs (cs1, cs2), merge_context_cs (ctxt_cs1, ctxt_cs2));
   28.17  );
   28.18  
    29.1 --- a/src/Pure/Isar/attrib.ML	Sun Nov 08 18:43:22 2009 +0100
    29.2 +++ b/src/Pure/Isar/attrib.ML	Sun Nov 08 18:43:42 2009 +0100
    29.3 @@ -65,13 +65,12 @@
    29.4  
    29.5  (* theory data *)
    29.6  
    29.7 -structure Attributes = TheoryDataFun
    29.8 +structure Attributes = Theory_Data
    29.9  (
   29.10    type T = ((src -> attribute) * string) Name_Space.table;
   29.11    val empty : T = Name_Space.empty_table "attribute";
   29.12 -  val copy = I;
   29.13    val extend = I;
   29.14 -  fun merge _ tables : T = Name_Space.merge_tables tables;
   29.15 +  fun merge data : T = Name_Space.merge_tables data;
   29.16  );
   29.17  
   29.18  fun print_attributes thy =
   29.19 @@ -321,13 +320,12 @@
   29.20  
   29.21  (* naming *)
   29.22  
   29.23 -structure Configs = TheoryDataFun
   29.24 +structure Configs = Theory_Data
   29.25  (
   29.26    type T = Config.value Config.T Symtab.table;
   29.27    val empty = Symtab.empty;
   29.28 -  val copy = I;
   29.29    val extend = I;
   29.30 -  fun merge _ = Symtab.merge (K true);
   29.31 +  fun merge data = Symtab.merge (K true) data;
   29.32  );
   29.33  
   29.34  fun print_configs ctxt =
    30.1 --- a/src/Pure/Isar/class_target.ML	Sun Nov 08 18:43:22 2009 +0100
    30.2 +++ b/src/Pure/Isar/class_target.ML	Sun Nov 08 18:43:42 2009 +0100
    30.3 @@ -105,13 +105,12 @@
    30.4      (Thm.merge_thms (defs1, defs2),
    30.5        AList.merge (op =) (K true) (operations1, operations2)));
    30.6  
    30.7 -structure ClassData = TheoryDataFun
    30.8 +structure ClassData = Theory_Data
    30.9  (
   30.10    type T = class_data Graph.T
   30.11    val empty = Graph.empty;
   30.12 -  val copy = I;
   30.13    val extend = I;
   30.14 -  fun merge _ = Graph.join merge_class_data;
   30.15 +  val merge = Graph.join merge_class_data;
   30.16  );
   30.17  
   30.18  
    31.1 --- a/src/Pure/Isar/code.ML	Sun Nov 08 18:43:22 2009 +0100
    31.2 +++ b/src/Pure/Isar/code.ML	Sun Nov 08 18:43:42 2009 +0100
    31.3 @@ -703,13 +703,12 @@
    31.4  
    31.5  (* c.f. src/HOL/Tools/recfun_codegen.ML *)
    31.6  
    31.7 -structure Code_Target_Attr = TheoryDataFun (
    31.8 +structure Code_Target_Attr = Theory_Data
    31.9 +(
   31.10    type T = (string -> thm -> theory -> theory) option;
   31.11    val empty = NONE;
   31.12 -  val copy = I;
   31.13    val extend = I;
   31.14 -  fun merge _ (NONE, f2) = f2
   31.15 -    | merge _ (f1, _) = f1;
   31.16 +  fun merge (f1, f2) = if is_some f1 then f1 else f2;
   31.17  );
   31.18  
   31.19  fun set_code_target_attr f = Code_Target_Attr.map (K (SOME f));
    32.1 --- a/src/Pure/Isar/locale.ML	Sun Nov 08 18:43:22 2009 +0100
    32.2 +++ b/src/Pure/Isar/locale.ML	Sun Nov 08 18:43:42 2009 +0100
    32.3 @@ -122,13 +122,12 @@
    32.4            merge (eq_snd op =) (notes, notes')),
    32.5              merge (eq_snd op =) (dependencies, dependencies')));
    32.6  
    32.7 -structure Locales = TheoryDataFun
    32.8 +structure Locales = Theory_Data
    32.9  (
   32.10    type T = locale Name_Space.table;
   32.11    val empty : T = Name_Space.empty_table "locale";
   32.12 -  val copy = I;
   32.13    val extend = I;
   32.14 -  fun merge _ = Name_Space.join_tables (K merge_locale);
   32.15 +  val merge = Name_Space.join_tables (K merge_locale);
   32.16  );
   32.17  
   32.18  val intern = Name_Space.intern o #1 o Locales.get;
   32.19 @@ -332,7 +331,7 @@
   32.20  
   32.21  (*** Registrations: interpretations in theories ***)
   32.22  
   32.23 -structure Registrations = TheoryDataFun
   32.24 +structure Registrations = Theory_Data
   32.25  (
   32.26    type T = ((string * (morphism * morphism)) * stamp) list *
   32.27      (* registrations, in reverse order of declaration *)
   32.28 @@ -340,8 +339,7 @@
   32.29      (* alist of mixin lists, per list mixins in reverse order of declaration *)
   32.30    val empty = ([], []);
   32.31    val extend = I;
   32.32 -  val copy = I;
   32.33 -  fun merge _ ((r1, m1), (r2, m2)) : T =
   32.34 +  fun merge ((r1, m1), (r2, m2)) : T =
   32.35      (Library.merge (eq_snd op =) (r1, r2),
   32.36        AList.join (op =) (K (Library.merge (eq_snd op =))) (m1, m2));
   32.37      (* FIXME consolidate with dependencies, consider one data slot only *)
    33.1 --- a/src/Pure/Isar/method.ML	Sun Nov 08 18:43:22 2009 +0100
    33.2 +++ b/src/Pure/Isar/method.ML	Sun Nov 08 18:43:42 2009 +0100
    33.3 @@ -320,13 +320,12 @@
    33.4  
    33.5  (* method definitions *)
    33.6  
    33.7 -structure Methods = TheoryDataFun
    33.8 +structure Methods = Theory_Data
    33.9  (
   33.10    type T = ((src -> Proof.context -> method) * string) Name_Space.table;
   33.11    val empty : T = Name_Space.empty_table "method";
   33.12 -  val copy = I;
   33.13    val extend = I;
   33.14 -  fun merge _ tables : T = Name_Space.merge_tables tables;
   33.15 +  fun merge data : T = Name_Space.merge_tables data;
   33.16  );
   33.17  
   33.18  fun print_methods thy =
    34.1 --- a/src/Pure/Isar/object_logic.ML	Sun Nov 08 18:43:22 2009 +0100
    34.2 +++ b/src/Pure/Isar/object_logic.ML	Sun Nov 08 18:43:42 2009 +0100
    34.3 @@ -47,18 +47,17 @@
    34.4  fun make_data (base_sort, judgment, atomize_rulify) =
    34.5    Data {base_sort = base_sort, judgment = judgment, atomize_rulify = atomize_rulify};
    34.6  
    34.7 -structure ObjectLogicData = TheoryDataFun
    34.8 +structure ObjectLogicData = Theory_Data
    34.9  (
   34.10    type T = data;
   34.11    val empty = make_data (NONE, NONE, ([], []));
   34.12 -  val copy = I;
   34.13    val extend = I;
   34.14  
   34.15    fun merge_opt eq (SOME x, SOME y) =
   34.16          if eq (x, y) then SOME x else error "Attempt to merge different object-logics"
   34.17      | merge_opt _ (x, y) = if is_some x then x else y;
   34.18  
   34.19 -  fun merge _
   34.20 +  fun merge
   34.21       (Data {base_sort = base_sort1, judgment = judgment1, atomize_rulify = (atomize1, rulify1)},
   34.22        Data {base_sort = base_sort2, judgment = judgment2, atomize_rulify = (atomize2, rulify2)}) =
   34.23      make_data (merge_opt (op =) (base_sort1, base_sort2), merge_opt (op =) (judgment1, judgment2),
    35.1 --- a/src/Pure/Proof/extraction.ML	Sun Nov 08 18:43:22 2009 +0100
    35.2 +++ b/src/Pure/Proof/extraction.ML	Sun Nov 08 18:43:42 2009 +0100
    35.3 @@ -167,7 +167,7 @@
    35.4  
    35.5  (* theory data *)
    35.6  
    35.7 -structure ExtractionData = TheoryDataFun
    35.8 +structure ExtractionData = Theory_Data
    35.9  (
   35.10    type T =
   35.11      {realizes_eqns : rules,
   35.12 @@ -187,20 +187,19 @@
   35.13       defs = [],
   35.14       expand = [],
   35.15       prep = NONE};
   35.16 -  val copy = I;
   35.17    val extend = I;
   35.18  
   35.19 -  fun merge _
   35.20 -    (({realizes_eqns = realizes_eqns1, typeof_eqns = typeof_eqns1, types = types1,
   35.21 +  fun merge
   35.22 +    ({realizes_eqns = realizes_eqns1, typeof_eqns = typeof_eqns1, types = types1,
   35.23         realizers = realizers1, defs = defs1, expand = expand1, prep = prep1},
   35.24        {realizes_eqns = realizes_eqns2, typeof_eqns = typeof_eqns2, types = types2,
   35.25 -       realizers = realizers2, defs = defs2, expand = expand2, prep = prep2}) : T * T) =
   35.26 +       realizers = realizers2, defs = defs2, expand = expand2, prep = prep2}) : T =
   35.27      {realizes_eqns = merge_rules realizes_eqns1 realizes_eqns2,
   35.28       typeof_eqns = merge_rules typeof_eqns1 typeof_eqns2,
   35.29       types = AList.merge (op =) (K true) (types1, types2),
   35.30       realizers = Symtab.merge_list (eq_set (op =) o pairself #1) (realizers1, realizers2),
   35.31       defs = Library.merge Thm.eq_thm (defs1, defs2),
   35.32 -     expand = Library.merge (op =) (expand1, expand2),
   35.33 +     expand = Library.merge (op =) (expand1, expand2),   (* FIXME proper aconv !?! *)
   35.34       prep = (case prep1 of NONE => prep2 | _ => prep1)};
   35.35  );
   35.36  
    36.1 --- a/src/Pure/Thy/present.ML	Sun Nov 08 18:43:22 2009 +0100
    36.2 +++ b/src/Pure/Thy/present.ML	Sun Nov 08 18:43:42 2009 +0100
    36.3 @@ -64,13 +64,12 @@
    36.4  
    36.5  (** additional theory data **)
    36.6  
    36.7 -structure BrowserInfoData = TheoryDataFun
    36.8 +structure BrowserInfoData = Theory_Data
    36.9  (
   36.10    type T = {name: string, session: string list, is_local: bool};
   36.11    val empty = {name = "", session = [], is_local = false}: T;
   36.12 -  val copy = I;
   36.13    fun extend _ = empty;
   36.14 -  fun merge _ _ = empty;
   36.15 +  fun merge _ = empty;
   36.16  );
   36.17  
   36.18  val put_info = BrowserInfoData.put;
    37.1 --- a/src/Pure/Thy/term_style.ML	Sun Nov 08 18:43:22 2009 +0100
    37.2 +++ b/src/Pure/Thy/term_style.ML	Sun Nov 08 18:43:42 2009 +0100
    37.3 @@ -19,13 +19,12 @@
    37.4  fun err_dup_style name =
    37.5    error ("Duplicate declaration of antiquote style: " ^ quote name);
    37.6  
    37.7 -structure StyleData = TheoryDataFun
    37.8 +structure StyleData = Theory_Data
    37.9  (
   37.10    type T = ((Proof.context -> term -> term) parser * stamp) Symtab.table;
   37.11    val empty = Symtab.empty;
   37.12 -  val copy = I;
   37.13    val extend = I;
   37.14 -  fun merge _ tabs : T = Symtab.merge (eq_snd (op =)) tabs
   37.15 +  fun merge data : T = Symtab.merge (eq_snd (op =)) data
   37.16      handle Symtab.DUP dup => err_dup_style dup;
   37.17  );
   37.18  
    38.1 --- a/src/Pure/Thy/thy_info.ML	Sun Nov 08 18:43:22 2009 +0100
    38.2 +++ b/src/Pure/Thy/thy_info.ML	Sun Nov 08 18:43:42 2009 +0100
    38.3 @@ -233,15 +233,14 @@
    38.4  
    38.5  (* management data *)
    38.6  
    38.7 -structure Management_Data = TheoryDataFun
    38.8 +structure Management_Data = Theory_Data
    38.9  (
   38.10    type T =
   38.11      Task_Queue.group option *   (*worker thread group*)
   38.12      int;                        (*abstract update time*)
   38.13    val empty = (NONE, 0);
   38.14 -  val copy = I;
   38.15    fun extend _ = empty;
   38.16 -  fun merge _ _ = empty;
   38.17 +  fun merge _ = empty;
   38.18  );
   38.19  
   38.20  val thy_ord = int_ord o pairself (#2 o Management_Data.get);
    39.1 --- a/src/Pure/codegen.ML	Sun Nov 08 18:43:22 2009 +0100
    39.2 +++ b/src/Pure/codegen.ML	Sun Nov 08 18:43:42 2009 +0100
    39.3 @@ -185,7 +185,7 @@
    39.4  
    39.5  (* theory data *)
    39.6  
    39.7 -structure CodegenData = TheoryDataFun
    39.8 +structure CodegenData = Theory_Data
    39.9  (
   39.10    type T =
   39.11      {codegens : (string * term codegen) list,
   39.12 @@ -198,16 +198,15 @@
   39.13    val empty =
   39.14      {codegens = [], tycodegens = [], consts = [], types = [],
   39.15       preprocs = [], modules = Symtab.empty};
   39.16 -  val copy = I;
   39.17    val extend = I;
   39.18  
   39.19 -  fun merge _
   39.20 +  fun merge
   39.21      ({codegens = codegens1, tycodegens = tycodegens1,
   39.22        consts = consts1, types = types1,
   39.23        preprocs = preprocs1, modules = modules1} : T,
   39.24       {codegens = codegens2, tycodegens = tycodegens2,
   39.25        consts = consts2, types = types2,
   39.26 -      preprocs = preprocs2, modules = modules2}) =
   39.27 +      preprocs = preprocs2, modules = modules2}) : T =
   39.28      {codegens = AList.merge (op =) (K true) (codegens1, codegens2),
   39.29       tycodegens = AList.merge (op =) (K true) (tycodegens1, tycodegens2),
   39.30       consts = AList.merge (op =) (K true) (consts1, consts2),
   39.31 @@ -287,13 +286,12 @@
   39.32      | _ => err ()
   39.33    end;
   39.34  
   39.35 -structure UnfoldData = TheoryDataFun
   39.36 +structure UnfoldData = Theory_Data
   39.37  (
   39.38    type T = simpset;
   39.39    val empty = empty_ss;
   39.40 -  val copy = I;
   39.41    val extend = I;
   39.42 -  fun merge _ = merge_ss;
   39.43 +  val merge = merge_ss;
   39.44  );
   39.45  
   39.46  val map_unfold = UnfoldData.map;
    40.1 --- a/src/Pure/interpretation.ML	Sun Nov 08 18:43:22 2009 +0100
    40.2 +++ b/src/Pure/interpretation.ML	Sun Nov 08 18:43:42 2009 +0100
    40.3 @@ -18,13 +18,12 @@
    40.4  
    40.5  type T = T;
    40.6  
    40.7 -structure Interp = TheoryDataFun
    40.8 +structure Interp = Theory_Data
    40.9  (
   40.10    type T = T list * (((T -> theory -> theory) * stamp) * T list) list;
   40.11    val empty = ([], []);
   40.12    val extend = I;
   40.13 -  val copy = I;
   40.14 -  fun merge _ ((data1, interps1), (data2, interps2)) : T =
   40.15 +  fun merge ((data1, interps1), (data2, interps2)) : T =
   40.16      (Library.merge eq (data1, data2),
   40.17       AList.join (eq_snd (op =)) (K (Library.merge eq)) (interps1, interps2));
   40.18  );
    41.1 --- a/src/Pure/proofterm.ML	Sun Nov 08 18:43:22 2009 +0100
    41.2 +++ b/src/Pure/proofterm.ML	Sun Nov 08 18:43:42 2009 +0100
    41.3 @@ -1247,14 +1247,13 @@
    41.4  
    41.5  (**** theory data ****)
    41.6  
    41.7 -structure ProofData = TheoryDataFun
    41.8 +structure ProofData = Theory_Data
    41.9  (
   41.10    type T = (stamp * (proof * proof)) list * (stamp * (typ list -> proof -> proof option)) list;
   41.11  
   41.12    val empty = ([], []);
   41.13 -  val copy = I;
   41.14    val extend = I;
   41.15 -  fun merge _ ((rules1, procs1), (rules2, procs2)) : T =
   41.16 +  fun merge ((rules1, procs1), (rules2, procs2)) : T =
   41.17      (AList.merge (op =) (K true) (rules1, rules2),
   41.18        AList.merge (op =) (K true) (procs1, procs2));
   41.19  );
    42.1 --- a/src/Pure/pure_thy.ML	Sun Nov 08 18:43:22 2009 +0100
    42.2 +++ b/src/Pure/pure_thy.ML	Sun Nov 08 18:43:42 2009 +0100
    42.3 @@ -54,13 +54,12 @@
    42.4  
    42.5  (** theory data **)
    42.6  
    42.7 -structure FactsData = TheoryDataFun
    42.8 +structure FactsData = Theory_Data
    42.9  (
   42.10    type T = Facts.T * thm list;
   42.11    val empty = (Facts.empty, []);
   42.12 -  val copy = I;
   42.13    fun extend (facts, _) = (facts, []);
   42.14 -  fun merge _ ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), []);
   42.15 +  fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), []);
   42.16  );
   42.17  
   42.18  
   42.19 @@ -246,13 +245,12 @@
   42.20    ("_applC", typ "('b => 'a) => cargs => logic", Mixfix ("(1_/ _)", [1000, 1000], 999)),
   42.21    ("_applC", typ "('b => 'a) => cargs => aprop", Mixfix ("(1_/ _)", [1000, 1000], 999))];
   42.22  
   42.23 -structure OldApplSyntax = TheoryDataFun
   42.24 +structure OldApplSyntax = Theory_Data
   42.25  (
   42.26    type T = bool;
   42.27    val empty = false;
   42.28 -  val copy = I;
   42.29    val extend = I;
   42.30 -  fun merge _ (b1, b2) : T =
   42.31 +  fun merge (b1, b2) : T =
   42.32      if b1 = b2 then b1
   42.33      else error "Cannot merge theories with different application syntax";
   42.34  );
   42.35 @@ -269,7 +267,7 @@
   42.36  
   42.37  val _ = Context.>> (Context.map_theory
   42.38    (Sign.map_naming (Name_Space.set_theory_name Context.PureN) #>
   42.39 -   OldApplSyntax.init #>
   42.40 +   OldApplSyntax.put false #>
   42.41     Sign.add_types
   42.42     [(Binding.name "fun", 2, NoSyn),
   42.43      (Binding.name "prop", 0, NoSyn),
    43.1 --- a/src/Pure/thm.ML	Sun Nov 08 18:43:22 2009 +0100
    43.2 +++ b/src/Pure/thm.ML	Sun Nov 08 18:43:42 2009 +0100
    43.3 @@ -1724,13 +1724,12 @@
    43.4  
    43.5  (* authentic derivation names *)
    43.6  
    43.7 -structure Oracles = TheoryDataFun
    43.8 +structure Oracles = Theory_Data
    43.9  (
   43.10    type T = unit Name_Space.table;
   43.11    val empty : T = Name_Space.empty_table "oracle";
   43.12 -  val copy = I;
   43.13    val extend = I;
   43.14 -  fun merge _ oracles : T = Name_Space.merge_tables oracles;
   43.15 +  fun merge data : T = Name_Space.merge_tables data;
   43.16  );
   43.17  
   43.18  val extern_oracles = map #1 o Name_Space.extern_table o Oracles.get;
    44.1 --- a/src/Tools/Code/code_preproc.ML	Sun Nov 08 18:43:22 2009 +0100
    44.2 +++ b/src/Tools/Code/code_preproc.ML	Sun Nov 08 18:43:42 2009 +0100
    44.3 @@ -56,13 +56,12 @@
    44.4        val functrans = AList.merge (op =) (eq_fst (op =)) (functrans1, functrans2);
    44.5      in make_thmproc ((pre, post), functrans) end;
    44.6  
    44.7 -structure Code_Preproc_Data = TheoryDataFun
    44.8 +structure Code_Preproc_Data = Theory_Data
    44.9  (
   44.10    type T = thmproc;
   44.11    val empty = make_thmproc ((Simplifier.empty_ss, Simplifier.empty_ss), []);
   44.12 -  fun copy spec = spec;
   44.13 -  val extend = copy;
   44.14 -  fun merge _ = merge_thmproc;
   44.15 +  val extend = I;
   44.16 +  val merge = merge_thmproc;
   44.17  );
   44.18  
   44.19  fun the_thmproc thy = case Code_Preproc_Data.get thy
    45.1 --- a/src/Tools/Code/code_target.ML	Sun Nov 08 18:43:22 2009 +0100
    45.2 +++ b/src/Tools/Code/code_target.ML	Sun Nov 08 18:43:42 2009 +0100
    45.3 @@ -148,13 +148,12 @@
    45.4    else
    45.5      error ("Incompatible serializers: " ^ quote target);
    45.6  
    45.7 -structure CodeTargetData = TheoryDataFun
    45.8 +structure CodeTargetData = Theory_Data
    45.9  (
   45.10    type T = target Symtab.table * string list;
   45.11    val empty = (Symtab.empty, []);
   45.12 -  val copy = I;
   45.13    val extend = I;
   45.14 -  fun merge _ ((target1, exc1) : T, (target2, exc2)) =
   45.15 +  fun merge ((target1, exc1), (target2, exc2)) : T =
   45.16      (Symtab.join (merge_target true) (target1, target2), Library.merge (op =) (exc1, exc2));
   45.17  );
   45.18  
    46.1 --- a/src/Tools/nbe.ML	Sun Nov 08 18:43:22 2009 +0100
    46.2 +++ b/src/Tools/nbe.ML	Sun Nov 08 18:43:42 2009 +0100
    46.3 @@ -37,13 +37,12 @@
    46.4  
    46.5  (** certificates and oracle for "trivial type classes" **)
    46.6  
    46.7 -structure Triv_Class_Data = TheoryDataFun
    46.8 +structure Triv_Class_Data = Theory_Data
    46.9  (
   46.10    type T = (class * thm) list;
   46.11    val empty = [];
   46.12 -  val copy = I;
   46.13    val extend = I;
   46.14 -  fun merge pp = AList.merge (op =) (K true);
   46.15 +  fun merge data : T = AList.merge (op =) (K true) data;
   46.16  );
   46.17  
   46.18  fun add_const_alias thm thy =
    47.1 --- a/src/Tools/quickcheck.ML	Sun Nov 08 18:43:22 2009 +0100
    47.2 +++ b/src/Tools/quickcheck.ML	Sun Nov 08 18:43:42 2009 +0100
    47.3 @@ -52,16 +52,16 @@
    47.4    make_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)),
    47.5      case default_type1 of NONE => default_type2 | _ => default_type1);
    47.6  
    47.7 -structure Data = TheoryDataFun(
    47.8 +structure Data = Theory_Data
    47.9 +(
   47.10    type T = (string * (Proof.context -> term -> int -> term list option)) list
   47.11      * test_params;
   47.12    val empty = ([], Test_Params { size = 10, iterations = 100, default_type = NONE });
   47.13 -  val copy = I;
   47.14    val extend = I;
   47.15 -  fun merge pp ((generators1, params1), (generators2, params2)) =
   47.16 -    (AList.merge (op = : string * string -> bool) (K true) (generators1, generators2),
   47.17 +  fun merge ((generators1, params1), (generators2, params2)) : T =
   47.18 +    (AList.merge (op =) (K true) (generators1, generators2),
   47.19        merge_test_params (params1, params2));
   47.20 -)
   47.21 +);
   47.22  
   47.23  val add_generator = Data.map o apfst o AList.update (op =);
   47.24  
    48.1 --- a/src/Tools/value.ML	Sun Nov 08 18:43:22 2009 +0100
    48.2 +++ b/src/Tools/value.ML	Sun Nov 08 18:43:42 2009 +0100
    48.3 @@ -15,12 +15,12 @@
    48.4  structure Value : VALUE =
    48.5  struct
    48.6  
    48.7 -structure Evaluator = TheoryDataFun(
    48.8 +structure Evaluator = Theory_Data
    48.9 +(
   48.10    type T = (string * (Proof.context -> term -> term)) list;
   48.11    val empty = [];
   48.12 -  val copy = I;
   48.13    val extend = I;
   48.14 -  fun merge _ data = AList.merge (op =) (K true) data;
   48.15 +  fun merge data : T = AList.merge (op =) (K true) data;
   48.16  )
   48.17  
   48.18  val add_evaluator = Evaluator.map o AList.update (op =);
    49.1 --- a/src/ZF/Tools/ind_cases.ML	Sun Nov 08 18:43:22 2009 +0100
    49.2 +++ b/src/ZF/Tools/ind_cases.ML	Sun Nov 08 18:43:42 2009 +0100
    49.3 @@ -18,13 +18,12 @@
    49.4  
    49.5  (* theory data *)
    49.6  
    49.7 -structure IndCasesData = TheoryDataFun
    49.8 +structure IndCasesData = Theory_Data
    49.9  (
   49.10    type T = (simpset -> cterm -> thm) Symtab.table;
   49.11    val empty = Symtab.empty;
   49.12 -  val copy = I;
   49.13    val extend = I;
   49.14 -  fun merge _ tabs : T = Symtab.merge (K true) tabs;
   49.15 +  fun merge data = Symtab.merge (K true) data;
   49.16  );
   49.17  
   49.18  
    50.1 --- a/src/ZF/Tools/induct_tacs.ML	Sun Nov 08 18:43:22 2009 +0100
    50.2 +++ b/src/ZF/Tools/induct_tacs.ML	Sun Nov 08 18:43:42 2009 +0100
    50.3 @@ -29,13 +29,12 @@
    50.4     mutual_induct : thm,
    50.5     exhaustion : thm};
    50.6  
    50.7 -structure DatatypesData = TheoryDataFun
    50.8 +structure DatatypesData = Theory_Data
    50.9  (
   50.10    type T = datatype_info Symtab.table;
   50.11    val empty = Symtab.empty;
   50.12 -  val copy = I;
   50.13    val extend = I;
   50.14 -  fun merge _ tabs : T = Symtab.merge (K true) tabs;
   50.15 +  fun merge data : T = Symtab.merge (K true) data;
   50.16  );
   50.17  
   50.18  
   50.19 @@ -49,13 +48,12 @@
   50.20     rec_rewrites : thm list};  (*recursor equations*)
   50.21  
   50.22  
   50.23 -structure ConstructorsData = TheoryDataFun
   50.24 +structure ConstructorsData = Theory_Data
   50.25  (
   50.26    type T = constructor_info Symtab.table
   50.27    val empty = Symtab.empty
   50.28 -  val copy = I;
   50.29    val extend = I
   50.30 -  fun merge _ tabs : T = Symtab.merge (K true) tabs;
   50.31 +  fun merge data = Symtab.merge (K true) data;
   50.32  );
   50.33  
   50.34  structure DatatypeTactics : DATATYPE_TACTICS =