changeset 33002 | f3f02f36a3e2 |
parent 31902 | 862ae16a799d |
child 33029 | 2fefe039edf1 |
--- a/src/Tools/atomize_elim.ML Mon Oct 19 16:47:21 2009 +0200 +++ b/src/Tools/atomize_elim.ML Mon Oct 19 21:54:57 2009 +0200 @@ -42,7 +42,7 @@ (* rearrange_prems as a conversion *) fun rearrange_prems_conv pi ct = let - val pi' = 0 :: map (curry op + 1) pi + val pi' = 0 :: map (Integer.add 1) pi val fwd = Thm.trivial ct |> Drule.rearrange_prems pi' val back = Thm.trivial (snd (Thm.dest_implies (cprop_of fwd)))