--- a/Nominal/nominal_inductive.ML	Tue Jun 12 14:22:58 2012 +0100
+++ b/Nominal/nominal_inductive.ML	Mon Jun 18 14:50:02 2012 +0100
@@ -430,7 +430,7 @@
   val main_parser = Parse.xname -- avoids_parser
 in
   val _ =
-    Outer_Syntax.local_theory_to_proof ("nominal_inductive", Keyword.thy_goal)
+    Outer_Syntax.local_theory_to_proof @{command_spec "nominal_inductive"}
       "prove strong induction theorem for inductive predicate involving nominal datatypes"
         (main_parser >> prove_strong_inductive_cmd)
 end