diff -r 0b217404522a -r dfc2e722fe47 src/HOL/NanoJava/Decl.thy
--- a/src/HOL/NanoJava/Decl.thy	Sun Aug 21 22:13:04 2011 +0200
+++ b/src/HOL/NanoJava/Decl.thy	Sun Aug 21 22:13:04 2011 +0200
@@ -44,9 +44,9 @@
   (type) "cdecl" \<leftharpoondown> (type) "cname \<times> class"
   (type) "prog " \<leftharpoondown> (type) "cdecl list"
 
-consts
-
+axiomatization
   Prog    :: prog       --{* program as a global value *}
+and
   Object  :: cname      --{* name of root class *}