
diff -r e46d4ee64221 -r 1b7c034c9e9e Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Tue Jun 12 14:22:58 2012 +0100
+++ b/Nominal/Nominal2.thy	Mon Jun 18 14:50:02 2012 +0100
@@ -748,7 +748,7 @@
 end
 
 (* Command Keyword *)
-val _ = Outer_Syntax.local_theory ("nominal_datatype", Keyword.thy_decl) 
+val _ = Outer_Syntax.local_theory @{command_spec "nominal_datatype"}
   "declaration of nominal datatypes" 
     (main_parser >> nominal_datatype2_cmd)
 *}




