--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML Mon Mar 28 12:05:47 2016 +0200
@@ -69,7 +69,8 @@
rtac ctxt cong_alg_intro) THEN
unfold_thms_tac ctxt (extra_simps @ sumprod_thms_rel @
@{thms vimage2p_def prod.rel_eq sum.rel_eq}) THEN
- REPEAT_DETERM (HEADGOAL (rtac ctxt conjI ORELSE' assume_tac ctxt ORELSE' rtac ctxt refl));
+ REPEAT_DETERM (HEADGOAL (etac ctxt subst ORELSE' rtac ctxt conjI ORELSE' assume_tac ctxt ORELSE'
+ rtac ctxt refl));
val shared_simps =
@{thms map_prod_simp map_sum.simps sum.case prod.case_eq_if split_beta' prod.sel