src/HOL/Tools/record.ML

       | NONE => raise THM ("named_cterm_instantiate: " ^ name, 0, [thm]));
   in
     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 =
   let
     fun get_thms thy name =

     records sel_upd equalities extinjects extsplit splits extfields fieldext =
  {records = records, sel_upd = sel_upd,
   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 =
     make_record_data Symtab.empty
       {selectors = Symtab.empty, updates = Symtab.empty,
           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,
        simpset = ss1, defset = ds1,
        foldcong = fc1, unfoldcong = uc1},

         simpset = Simplifier.merge_ss (ss1, ss2),
         defset = Simplifier.merge_ss (ds1, ds2),
         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
           Thm.eq_thm (c, y) andalso Thm.eq_thm (d, z)) (splits1, splits2))
       (Symtab.merge (K true) (extfields1, extfields2))