--- a/src/HOL/Nominal/nominal_induct.ML Fri Aug 23 15:36:54 2013 +0200
+++ b/src/HOL/Nominal/nominal_induct.ML Fri Aug 23 17:01:12 2013 +0200
@@ -169,8 +169,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)));