--- a/src/HOL/Tools/inductive_set_package.ML Thu Jan 01 14:23:39 2009 +0100
+++ b/src/HOL/Tools/inductive_set_package.ML Thu Jan 01 14:23:39 2009 +0100
@@ -169,7 +169,7 @@
({to_set_simps = to_set_simps1, to_pred_simps = to_pred_simps1,
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}) =
+ set_arities = set_arities2, pred_arities = pred_arities2}) : T =
{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),