src/HOL/Tools/inductive_set_package.ML
changeset 29288 253bcf2a5854
parent 29064 70a61d58460e
child 29389 0a49f940d729
     1.1 --- a/src/HOL/Tools/inductive_set_package.ML	Thu Jan 01 14:23:39 2009 +0100
     1.2 +++ b/src/HOL/Tools/inductive_set_package.ML	Thu Jan 01 14:23:39 2009 +0100
     1.3 @@ -169,7 +169,7 @@
     1.4      ({to_set_simps = to_set_simps1, to_pred_simps = to_pred_simps1,
     1.5        set_arities = set_arities1, pred_arities = pred_arities1},
     1.6       {to_set_simps = to_set_simps2, to_pred_simps = to_pred_simps2,
     1.7 -      set_arities = set_arities2, pred_arities = pred_arities2}) =
     1.8 +      set_arities = set_arities2, pred_arities = pred_arities2}) : T =
     1.9      {to_set_simps = Thm.merge_thms (to_set_simps1, to_set_simps2),
    1.10       to_pred_simps = Thm.merge_thms (to_pred_simps1, to_pred_simps2),
    1.11       set_arities = Symtab.merge_list op = (set_arities1, set_arities2),