diff -r 14c7d7e29c44 -r 87d1e815aa59 Nominal/nominal_termination.ML
--- a/Nominal/nominal_termination.ML	Sun Jul 15 13:03:47 2012 +0100
+++ b/Nominal/nominal_termination.ML	Fri Aug 03 14:46:25 2012 +0200
@@ -106,7 +106,7 @@
      (Parse.reserved "no_eqvt" >> K (true, false))) --| @{keyword ")"}) (false, false))
 
 val _ =
-  Outer_Syntax.local_theory_to_proof ("termination", Keyword.thy_goal) 
+  Outer_Syntax.local_theory_to_proof @{command_spec "termination"}
     "prove termination of a recursive function"
       (option_parser -- Scan.option Parse.term >> 
         (fn ((is_nominal, is_eqvt), opt_trm) =>