--- a/Nominal/Nominal2.thy	Sat Mar 17 05:13:59 2012 +0000
+++ b/Nominal/Nominal2.thy	Tue Mar 20 11:26:10 2012 +0000
@@ -710,8 +710,6 @@
   fun tuple3 ((x, y), (z, u)) = (x, y, z, u)
 in
 
-val _ = Keyword.keyword "binds"
-
 val opt_name = Scan.option (P.binding --| Args.colon)
 
 val anno_typ = S.option (P.name --| @{keyword "::"}) -- P.typ
@@ -742,8 +740,9 @@
 end
 
 (* Command Keyword *)
-val _ = Outer_Syntax.local_theory "nominal_datatype" "test" Keyword.thy_decl
-  (main_parser >> nominal_datatype2_cmd)
+val _ = Outer_Syntax.local_theory ("nominal_datatype", Keyword.thy_decl) 
+  "declaration of nominal datatypes" 
+    (main_parser >> nominal_datatype2_cmd)
 *}