--- a/src/HOL/Tools/inductive_set_package.ML Sun Jul 29 14:29:52 2007 +0200
+++ b/src/HOL/Tools/inductive_set_package.ML Sun Jul 29 14:29:54 2007 +0200
@@ -172,8 +172,8 @@
set_arities = set_arities1, pred_arities = pred_arities1},
{to_set_simps = to_set_simps2, to_pred_simps = to_pred_simps2,
set_arities = set_arities2, pred_arities = pred_arities2}) =
- {to_set_simps = Drule.merge_rules (to_set_simps1, to_set_simps2),
- to_pred_simps = Drule.merge_rules (to_pred_simps1, to_pred_simps2),
+ {to_set_simps = Thm.merge_thms (to_set_simps1, to_set_simps2),
+ to_pred_simps = Thm.merge_thms (to_pred_simps1, to_pred_simps2),
set_arities = Symtab.merge_list op = (set_arities1, set_arities2),
pred_arities = Symtab.merge_list op = (pred_arities1, pred_arities2)};
);