diff -r 5ebd327ffb96 -r e2da10806a34 Nominal/nominal_termination.ML
--- a/Nominal/nominal_termination.ML	Mon May 19 12:45:26 2014 +0100
+++ b/Nominal/nominal_termination.ML	Mon May 19 16:45:46 2014 +0100
@@ -103,14 +103,13 @@
 
 val option_parser =
   (Scan.optional (@{keyword "("} |-- Parse.!!! 
-    ((Parse.reserved "eqvt" >> K (true, true)) ||
-     (Parse.reserved "no_eqvt" >> K (true, false))) --| @{keyword ")"}) (false, false))
+    ((Parse.reserved "eqvt" >> K true) ||
+     (Parse.reserved "no_eqvt" >> K false)) --| @{keyword ")"}) (false))
 
 val _ =
-  Outer_Syntax.local_theory_to_proof @{command_spec "termination"}
-    "prove termination of a recursive function"
+  Outer_Syntax.local_theory_to_proof @{command_spec "nominal_termination"}
+    "prove termination of a recursive nominal function"
       (option_parser -- Scan.option Parse.term >> 
-        (fn ((is_nominal, is_eqvt), opt_trm) => 
-           if is_nominal then termination_cmd is_eqvt opt_trm else Function.termination_cmd opt_trm))
+        (fn (is_eqvt, opt_trm) => termination_cmd is_eqvt opt_trm))
 
 end