diff -r f075640b8868 -r 3abf6a722518 src/HOL/NanoJava/Decl.thy
--- a/src/HOL/NanoJava/Decl.thy	Tue Jan 16 09:12:16 2018 +0100
+++ b/src/HOL/NanoJava/Decl.thy	Tue Jan 16 09:30:00 2018 +0100
@@ -8,8 +8,8 @@
 theory Decl imports Term begin
 
 datatype ty
-  = NT           \<comment>\<open>null type\<close>
-  | Class cname  \<comment>\<open>class type\<close>
+  = NT           \<comment> \<open>null type\<close>
+  | Class cname  \<comment> \<open>class type\<close>
 
 text\<open>Field declaration\<close>
 type_synonym fdecl           
@@ -45,9 +45,9 @@
   (type) "prog " \<leftharpoondown> (type) "cdecl list"
 
 axiomatization
-  Prog    :: prog       \<comment>\<open>program as a global value\<close>
+  Prog    :: prog       \<comment> \<open>program as a global value\<close>
 and
-  Object  :: cname      \<comment>\<open>name of root class\<close>
+  Object  :: cname      \<comment> \<open>name of root class\<close>
 
 
 definition "class" :: "cname \<rightharpoonup> class" where