--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML Fri Sep 27 19:30:49 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML Fri Sep 27 20:13:35 2013 +0200
@@ -71,7 +71,8 @@
exclsss =
mk_primcorec_prelude ctxt defs (f_sel RS trans) THEN
mk_primcorec_cases_tac ctxt k m exclsss THEN
- unfold_thms_tac ctxt (@{thms o_def split_def sum.cases} @ maps @ map_comps @ map_idents) THEN
+ unfold_thms_tac ctxt (@{thms id_apply o_def split_def sum.cases} @ maps @ map_comps @
+ map_idents) THEN
HEADGOAL (REPEAT_DETERM o (rtac refl ORELSE'
eresolve_tac falseEs ORELSE'
resolve_tac split_connectI ORELSE'
@@ -112,5 +113,4 @@
etac notE THEN' atac ORELSE'
(TRY o dresolve_tac disc_excludes) THEN' etac notE THEN' atac));
-
end;