diff -r 0fd80c27fdf5 -r f270e3e18be5 src/HOL/UNITY/Comp/Counterc.thy
--- a/src/HOL/UNITY/Comp/Counterc.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/UNITY/Comp/Counterc.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -30,7 +30,7 @@
   "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"
+type_synonym command = "(state*state)set"
 
 definition a :: "nat=>command" where
  "a i = {(s, s'). (c s') i = (c s) i + 1 & (C s') = (C s) + 1}"