changeset 24039 | 273698405054 |
parent 22846 | fb79144af9a3 |
child 24826 | 78e6a3cea367 |
--- a/src/ZF/Tools/typechk.ML Sun Jul 29 14:29:52 2007 +0200 +++ b/src/ZF/Tools/typechk.ML Sun Jul 29 14:29:54 2007 +0200 @@ -49,7 +49,7 @@ val extend = I; fun merge _ (TC {rules, net}, TC {rules = rules', net = net'}) = - TC {rules = Drule.merge_rules (rules, rules'), + TC {rules = Thm.merge_thms (rules, rules'), net = Net.merge Thm.eq_thm_prop (net, net')}; );