diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/UNITY/Comp/Counterc.ML
--- a/src/HOL/UNITY/Comp/Counterc.ML	Mon Oct 22 11:01:30 2001 +0200
+++ b/src/HOL/UNITY/Comp/Counterc.ML	Mon Oct 22 11:54:22 2001 +0200
@@ -38,7 +38,7 @@
 qed_spec_mp "sumj_ext";
 
 
-Goal "(ALL i. i<I --> c s i = Numeral0) -->  sum I s = Numeral0";
+Goal "(ALL i. i<I --> c s i = 0) -->  sum I s = 0";
 by (induct_tac "I" 1);
 by Auto_tac;
 qed "sum0";