src/HOL/Divides.thy

--- a/src/HOL/Divides.thy	Fri Sep 23 21:02:13 2005 +0200
+++ b/src/HOL/Divides.thy	Fri Sep 23 22:21:49 2005 +0200
@@ -201,7 +201,7 @@
 
 val prove_eq_sums =
   let val simps = add_0 :: add_0_right :: add_ac
-  in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all simps) end
+  in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all_tac simps) end;
 
 end;