Nominal/Nominal2.thy
changeset 3190 1b7c034c9e9e
parent 3181 ca162f0a7957
child 3201 3e6f4320669f
--- 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)
 *}