| changeset 30496 | 7cdcc9dd95cb |
| parent 30323 | 6a02238da8e9 |
| child 30517 | 51a39ed24c0f |
--- a/src/HOL/IntDiv.thy Thu Mar 12 18:01:25 2009 +0100 +++ b/src/HOL/IntDiv.thy Thu Mar 12 18:01:26 2009 +0100 @@ -261,7 +261,7 @@ val prove_eq_sums = let val simps = @{thm diff_int_def} :: Int_Numeral_Simprocs.add_0s @ @{thms zadd_ac} - in ArithData.prove_conv all_tac (ArithData.simp_all_tac simps) end; + in Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac simps) end; end) in