1.1 --- a/src/HOL/IntDiv.thy	Thu Mar 12 18:01:25 2009 +0100
     1.2 +++ b/src/HOL/IntDiv.thy	Thu Mar 12 18:01:26 2009 +0100
     1.3 @@ -261,7 +261,7 @@
     1.4    val prove_eq_sums =
     1.5      let
     1.6        val simps = @{thm diff_int_def} :: Int_Numeral_Simprocs.add_0s @ @{thms zadd_ac}
     1.7 -    in ArithData.prove_conv all_tac (ArithData.simp_all_tac simps) end;
     1.8 +    in Arith_Data.prove_conv2 all_tac (Arith_Data.simp_all_tac simps) end;
     1.9  end)
    1.10  
    1.11  in