--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Fri Mar 07 22:19:52 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Fri Mar 07 22:30:58 2014 +0100
@@ -140,7 +140,7 @@
(CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms fst_conv snd_conv id_def comp_def split_def
sum.case} @ mapsx @ map_comps @ map_idents))) ORELSE'
fo_rtac @{thm cong} ctxt ORELSE'
- rtac ext));
+ rtac @{thm ext}));
fun mk_primcorec_ctr_tac ctxt m collapse disc_fun_opt sel_funs =
HEADGOAL (rtac ((if null sel_funs then collapse else collapse RS sym) RS trans) THEN'