--- a/src/HOL/Nominal/nominal_induct.ML Sun Nov 09 14:08:00 2014 +0100
+++ b/src/HOL/Nominal/nominal_induct.ML Sun Nov 09 17:04:14 2014 +0100
@@ -127,7 +127,7 @@
(rtac (rename_params_rule false [] rule') i THEN
PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st'))))
THEN_ALL_NEW_CASES
- ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac)
+ ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac ctxt)
else K all_tac)
THEN_ALL_NEW Induct.rulify_tac ctxt)
end;