--- a/src/HOL/IMP/Expr.thy Wed Mar 30 22:53:18 2011 +0200
+++ b/src/HOL/IMP/Expr.thy Wed Mar 30 23:26:40 2011 +0200
@@ -14,8 +14,7 @@
subsection "Arithmetic expressions"
typedecl loc
-types
- state = "loc => nat"
+type_synonym state = "loc => nat"
datatype
aexp = N nat