# HG changeset patch
# User wenzelm
# Date 1475825351 -7200
# Node ID 21b83e8121aa22e6ca2187d33b4b88921328b298
# Parent  800174511cc32af14874ca0ced867fe1b05e3ef7# Parent  a480dd2fcfd82d2826ad1c60bc3f943252cbe764
merged

diff -r a480dd2fcfd8 -r 21b83e8121aa src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Oct 06 17:40:59 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Oct 07 09:29:11 2016 +0200
@@ -847,7 +847,7 @@
           in
             Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
               mk_map_tac ctxt abs_inverses pre_map_def dtor_ctor fp_map_thm'
-                live_nesting_map_ident0s ctr_defs' extra_unfolds_map)
+                live_nesting_map_id0s ctr_defs' extra_unfolds_map)
             |> Thm.close_derivation
             |> Conjunction.elim_balanced (length goals)
           end;
diff -r a480dd2fcfd8 -r 21b83e8121aa src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Thu Oct 06 17:40:59 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Fri Oct 07 09:29:11 2016 +0200
@@ -392,12 +392,12 @@
       (1 upto nn) ns pre_rel_defs fp_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss discsss
       selsss));
 
-fun mk_map_tac ctxt abs_inverses pre_map_def dtor_ctor fp_map' live_nesting_map_ident0s ctr_defs'
+fun mk_map_tac ctxt abs_inverses pre_map_def dtor_ctor fp_map' live_nesting_map_id0s ctr_defs'
     extra_unfolds =
   TRYALL Goal.conjunction_tac THEN
   unfold_thms_tac ctxt (pre_map_def :: dtor_ctor :: fp_map' :: abs_inverses @
-    live_nesting_map_ident0s @ ctr_defs' @ extra_unfolds @ sumprod_thms_map @
-    @{thms o_def[abs_def] id_def}) THEN
+    live_nesting_map_id0s @ ctr_defs' @ extra_unfolds @ sumprod_thms_map @
+    @{thms o_apply id_apply id_o o_id}) THEN
   ALLGOALS (rtac ctxt refl);
 
 fun mk_map_disc_iff_tac ctxt ct exhaust discs maps =