--- a/Nominal/nominal_induct.ML	Wed Jul 31 13:15:29 2013 +0100
+++ b/Nominal/nominal_induct.ML	Fri Aug 30 14:35:37 2013 +0100
@@ -173,8 +173,9 @@
 in
 
 val nominal_induct_method =
-  Args.mode Induct.no_simpN -- (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
-  avoiding -- fixing -- rule_spec) >>
+  Scan.lift (Args.mode Induct.no_simpN) -- 
+    (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
+      avoiding -- fixing -- rule_spec) >>
   (fn (no_simp, (((x, y), z), w)) => fn ctxt =>
     RAW_METHOD_CASES (fn facts =>
       HEADGOAL (nominal_induct_tac ctxt (not no_simp) x y z w facts)));