1.1 --- a/src/HOL/UNITY/Comp/Counterc.ML	Mon Oct 22 11:01:30 2001 +0200
     1.2 +++ b/src/HOL/UNITY/Comp/Counterc.ML	Mon Oct 22 11:54:22 2001 +0200
     1.3 @@ -38,7 +38,7 @@
     1.4  qed_spec_mp "sumj_ext";
     1.5  
     1.6  
     1.7 -Goal "(ALL i. i<I --> c s i = Numeral0) -->  sum I s = Numeral0";
     1.8 +Goal "(ALL i. i<I --> c s i = 0) -->  sum I s = 0";
     1.9  by (induct_tac "I" 1);
    1.10  by Auto_tac;
    1.11  qed "sum0";