diff -r 76401b2ee871 -r 56db9f3a6b3e src/HOL/UNITY/Comp/Counterc.thy
--- a/src/HOL/UNITY/Comp/Counterc.thy	Mon Oct 22 11:01:30 2001 +0200
+++ b/src/HOL/UNITY/Comp/Counterc.thy	Mon Oct 22 11:54:22 2001 +0200
@@ -24,20 +24,20 @@
   sumj :: "[nat, nat, state]=>int"
 
 primrec (* sum I s = sigma_{i<I}. c s i *)
-  "sum 0 s = Numeral0"
+  "sum 0 s = 0"
   "sum (Suc i) s = (c s) i + sum i s"
 
 primrec
-  "sumj 0 i s = Numeral0"
+  "sumj 0 i s = 0"
   "sumj (Suc n) i s = (if n=i then sum n s else (c s) n + sumj n i s)"
   
 types command = "(state*state)set"
 
 constdefs
   a :: "nat=>command"
- "a i == {(s, s'). (c s') i = (c s) i + Numeral1 & (C s') = (C s) + Numeral1}"
+ "a i == {(s, s'). (c s') i = (c s) i + 1 & (C s') = (C s) + 1}"
  
   Component :: "nat => state program"
-  "Component i == mk_program({s. C s = Numeral0 & (c s) i = Numeral0}, {a i},
+  "Component i == mk_program({s. C s = 0 & (c s) i = 0}, {a i},
 	       UN G: preserves (%s. (c s) i). Acts G)"
 end