--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Wed Jun 18 17:42:24 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Wed Jun 18 17:42:24 2014 +0200
@@ -138,7 +138,8 @@
eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE'
etac notE THEN' atac ORELSE'
(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'
+ sum.case sum.sel sum.distinct[THEN eq_False[THEN iffD2]]} @
+ mapsx @ map_comps @ map_idents))) ORELSE'
fo_rtac @{thm cong} ctxt ORELSE'
rtac @{thm ext}));