--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Fri Dec 13 23:53:02 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Sat Dec 14 17:28:05 2013 +0100
@@ -130,7 +130,7 @@
REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)]) THEN
EVERY [REPEAT_DETERM_N r
(HEADGOAL (rotate_tac ~1 THEN' dtac meta_mp THEN' rotate_tac 1) THEN prefer_tac 2),
- if r > 0 then ALLGOALS Goal.norm_hhf_tac else all_tac, HEADGOAL atac,
+ if r > 0 then ALLGOALS (Goal.norm_hhf_tac ctxt) else all_tac, HEADGOAL atac,
mk_induct_leverage_prem_prems_tac ctxt nn kks set_maps pre_set_defs]
end;