diff -r 5b0bfd63b5da -r 253bcf2a5854 src/HOL/Tools/inductive_set_package.ML
--- 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),