--- a/src/HOL/Nominal/nominal_induct.ML Mon Aug 18 15:46:27 2014 +0200
+++ b/src/HOL/Nominal/nominal_induct.ML Tue Aug 19 12:05:11 2014 +0200
@@ -172,9 +172,8 @@
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)));
+ (fn (no_simp, (((x, y), z), w)) => fn ctxt => fn facts =>
+ HEADGOAL (nominal_induct_tac ctxt (not no_simp) x y z w facts));
end;