diff -r b2e1a7b83e05 -r 67370521c09c Nominal/nominal_termination.ML
--- a/Nominal/nominal_termination.ML	Tue Jul 08 11:18:31 2014 +0100
+++ b/Nominal/nominal_termination.ML	Thu Jul 09 02:32:46 2015 +0100
@@ -26,7 +26,7 @@
 val simp_attribs = map (Attrib.internal o K)
   [Simplifier.simp_add,
    Code.add_default_eqn_attribute,
-   Nitpick_Simps.add]
+   Named_Theorems.add @{named_theorems nitpick_simp}]
 
 val eqvt_attrib =  Attrib.internal (K Nominal_ThmDecls.eqvt_add)
 
@@ -107,7 +107,7 @@
      (Parse.reserved "no_eqvt" >> K false)) --| @{keyword ")"}) (false))
 
 val _ =
-  Outer_Syntax.local_theory_to_proof @{command_spec "nominal_termination"}
+  Outer_Syntax.local_theory_to_proof @{command_keyword nominal_termination}
     "prove termination of a recursive nominal function"
       (option_parser -- Scan.option Parse.term >> 
         (fn (is_eqvt, opt_trm) => termination_cmd is_eqvt opt_trm))