diff -r e46d4ee64221 -r 1b7c034c9e9e Nominal/nominal_function.ML
--- a/Nominal/nominal_function.ML	Tue Jun 12 14:22:58 2012 +0100
+++ b/Nominal/nominal_function.ML	Mon Jun 18 14:50:02 2012 +0100
@@ -274,7 +274,7 @@
 
 (* nominal *)
 val _ =
-  Outer_Syntax.local_theory_to_proof' ("nominal_primrec", Keyword.thy_goal) 
+  Outer_Syntax.local_theory_to_proof' @{command_spec "nominal_primrec"}
     "define general recursive nominal functions"
        (nominal_function_parser nominal_default_config
           >> (fn ((config, fixes), statements) => nominal_function_cmd fixes statements config))