src/HOL/Tools/record_package.ML
changeset 6556 daa00919502b
parent 6519 5bd1c469e742
child 6723 f342449d73ca
equal deleted inserted replaced
6555:17b7b88a8e3c 6556:daa00919502b
   336   type T =
   336   type T =
   337     record_info Symtab.table *                          (*records*)
   337     record_info Symtab.table *                          (*records*)
   338       (thm Symtab.table * Simplifier.simpset);          (*field split rules*)
   338       (thm Symtab.table * Simplifier.simpset);          (*field split rules*)
   339 
   339 
   340   val empty = (Symtab.empty, (Symtab.empty, HOL_basic_ss));
   340   val empty = (Symtab.empty, (Symtab.empty, HOL_basic_ss));
       
   341   val copy = I;
   341   val prep_ext = I;
   342   val prep_ext = I;
   342   fun merge ((recs1, (sps1, ss1)), (recs2, (sps2, ss2))) =
   343   fun merge ((recs1, (sps1, ss1)), (recs2, (sps2, ss2))) =
   343     (Symtab.merge (K true) (recs1, recs2),
   344     (Symtab.merge (K true) (recs1, recs2),
   344       (Symtab.merge (K true) (sps1, sps2), Simplifier.merge_ss (ss1, ss2)));
   345       (Symtab.merge (K true) (sps1, sps2), Simplifier.merge_ss (ss1, ss2)));
   345 
   346