src/HOL/Tools/recdef.ML
changeset 33699 f33b036ef318
parent 33643 b275f26a638b
child 34952 bd7e347eb768
equal deleted inserted replaced
33698:b5f36fa5a7b4 33699:f33b036ef318
    94   fun merge
    94   fun merge
    95    ((tab1, {simps = simps1, congs = congs1, wfs = wfs1}),
    95    ((tab1, {simps = simps1, congs = congs1, wfs = wfs1}),
    96     (tab2, {simps = simps2, congs = congs2, wfs = wfs2})) : T =
    96     (tab2, {simps = simps2, congs = congs2, wfs = wfs2})) : T =
    97       (Symtab.merge (K true) (tab1, tab2),
    97       (Symtab.merge (K true) (tab1, tab2),
    98         mk_hints (Thm.merge_thms (simps1, simps2),
    98         mk_hints (Thm.merge_thms (simps1, simps2),
    99           AList.merge (op =) Thm.eq_thm_prop (congs1, congs2),
    99           AList.merge (op =) (K true) (congs1, congs2),
   100           Thm.merge_thms (wfs1, wfs2)));
   100           Thm.merge_thms (wfs1, wfs2)));
   101 );
   101 );
   102 
   102 
   103 val get_recdef = Symtab.lookup o #1 o GlobalRecdefData.get;
   103 val get_recdef = Symtab.lookup o #1 o GlobalRecdefData.get;
   104 
   104