renamed BNF axiom

--- a/src/HOL/BNF/More_BNFs.thy	Thu Aug 29 18:31:23 2013 +0200
+++ b/src/HOL/BNF/More_BNFs.thy	Thu Aug 29 18:44:03 2013 +0200
@@ -376,7 +376,7 @@
   qed
 qed
 
-lemma mmap_id: "mmap id = id"
+lemma mmap_id0: "mmap id = id"
 proof (intro ext multiset_eqI)
   fix f a show "count (mmap id f) a = count (id f) a"
   proof (cases "count f a = 0")
@@ -872,7 +872,7 @@
     (auto intro!: ordLess_imp_ordLeq simp: finite_iff_ordLess_natLeq[symmetric] multiset_def)
 
 bnf mmap [set_of] "\<lambda>_::'a multiset. natLeq" ["{#}"]
-by (auto simp add: mmap_id mmap_comp set_of_mmap natLeq_card_order natLeq_cinfinite set_of_bd
+by (auto simp add: mmap_id0 mmap_comp set_of_mmap natLeq_card_order natLeq_cinfinite set_of_bd
   intro: mmap_cong wpull_mmap)
 
 inductive multiset_rel' where

--- a/src/HOL/BNF/Tools/bnf_comp.ML	Thu Aug 29 18:31:23 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML	Thu Aug 29 18:44:03 2013 +0200
@@ -149,9 +149,9 @@
     (*(inner_1.bd +c ... +c inner_m.bd) *c outer.bd*)
     val bd = Term.absdummy CCA (mk_cprod (Library.foldr1 (uncurry mk_csum) inner_bds) outer_bd);
 
-    fun map_id_tac _ =
-      mk_comp_map_id_tac (map_id_of_bnf outer) (map_cong0_of_bnf outer)
-        (map map_id_of_bnf inners);
+    fun map_id0_tac _ =
+      mk_comp_map_id0_tac (map_id0_of_bnf outer) (map_cong0_of_bnf outer)
+        (map map_id0_of_bnf inners);
 
     fun map_comp_tac _ =
       mk_comp_map_comp_tac (map_comp_of_bnf outer) (map_cong0_of_bnf outer)
@@ -233,7 +233,7 @@
         rtac thm 1
       end;
 
-    val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
+    val tacs = zip_axioms map_id0_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
       bd_cinfinite_tac set_bd_tacs map_wpull_tac rel_OO_Grp_tac;
 
     val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer;
@@ -300,7 +300,7 @@
     val bd = mk_cprod
       (Library.foldr1 (uncurry mk_csum) (map (mk_card_of o HOLogic.mk_UNIV) killedAs)) bnf_bd;
 
-    fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
+    fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1;
     fun map_comp_tac {context = ctxt, prems = _} =
       unfold_thms_tac ctxt ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
       rtac refl 1;
@@ -339,7 +339,7 @@
         rtac thm 1
       end;
 
-    val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
+    val tacs = zip_axioms map_id0_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
       bd_cinfinite_tac set_bd_tacs map_wpull_tac rel_OO_Grp_tac;
 
     val bnf_wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf;
@@ -390,7 +390,7 @@
 
     val bd = mk_bd_of_bnf Ds As bnf;
 
-    fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
+    fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1;
     fun map_comp_tac {context = ctxt, prems = _} =
       unfold_thms_tac ctxt ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
       rtac refl 1;
@@ -424,7 +424,7 @@
 
     fun rel_OO_Grp_tac _ = mk_simple_rel_OO_Grp_tac (rel_OO_Grp_of_bnf bnf) in_alt_thm;
 
-    val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
+    val tacs = zip_axioms map_id0_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
       bd_cinfinite_tac set_bd_tacs map_wpull_tac rel_OO_Grp_tac;
 
     val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
@@ -474,7 +474,7 @@
 
     val bd = mk_bd_of_bnf Ds As bnf;
 
-    fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
+    fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1;
     fun map_comp_tac _ = rtac (map_comp_of_bnf bnf) 1;
     fun map_cong0_tac {context = ctxt, prems = _} =
       rtac (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1);
@@ -497,7 +497,7 @@
 
     fun rel_OO_Grp_tac _ = mk_simple_rel_OO_Grp_tac (rel_OO_Grp_of_bnf bnf) in_alt_thm;
 
-    val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
+    val tacs = zip_axioms map_id0_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
       bd_cinfinite_tac set_bd_tacs map_wpull_tac rel_OO_Grp_tac;
 
     val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
@@ -630,7 +630,7 @@
       (rtac (unfold_all thm) THEN'
       SOLVE o REPEAT_DETERM o (atac ORELSE' Goal.assume_rule_tac ctxt)) 1;
 
-    val tacs = zip_axioms (mk_tac (map_id_of_bnf bnf)) (mk_tac (map_comp_of_bnf bnf))
+    val tacs = zip_axioms (mk_tac (map_id0_of_bnf bnf)) (mk_tac (map_comp_of_bnf bnf))
       (mk_tac (map_cong0_of_bnf bnf)) (map mk_tac (set_map_of_bnf bnf))
       (K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1)) (map mk_tac set_bds)
       (mk_tac (map_wpull_of_bnf bnf))

--- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML	Thu Aug 29 18:31:23 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML	Thu Aug 29 18:44:03 2013 +0200
@@ -13,7 +13,7 @@
   val mk_comp_in_alt_tac: Proof.context -> thm list -> tactic
   val mk_comp_map_comp_tac: thm -> thm -> thm list -> tactic
   val mk_comp_map_cong0_tac: thm list -> thm -> thm list -> tactic
-  val mk_comp_map_id_tac: thm -> thm -> thm list -> tactic
+  val mk_comp_map_id0_tac: thm -> thm -> thm list -> tactic
   val mk_comp_set_alt_tac: Proof.context -> thm -> tactic
   val mk_comp_set_bd_tac: Proof.context -> thm -> thm list -> tactic
   val mk_comp_set_map_tac: thm -> thm -> thm -> thm list -> tactic
@@ -58,9 +58,9 @@
   unfold_thms_tac ctxt [collect_set_map RS sym] THEN
   rtac refl 1;
 
-fun mk_comp_map_id_tac Gmap_id Gmap_cong0 map_ids =
+fun mk_comp_map_id0_tac Gmap_id0 Gmap_cong0 map_id0s =
   EVERY' ([rtac ext, rtac (Gmap_cong0 RS trans)] @
-    map (fn thm => rtac (thm RS fun_cong)) map_ids @ [rtac (Gmap_id RS fun_cong)]) 1;
+    map (fn thm => rtac (thm RS fun_cong)) map_id0s @ [rtac (Gmap_id0 RS fun_cong)]) 1;
 
 fun mk_comp_map_comp_tac Gmap_comp Gmap_cong0 map_comps =
   EVERY' ([rtac ext, rtac sym, rtac trans_o_apply,

--- a/src/HOL/BNF/Tools/bnf_def.ML	Thu Aug 29 18:31:23 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Thu Aug 29 18:44:03 2013 +0200
@@ -55,8 +55,8 @@
   val map_cong0_of_bnf: bnf -> thm
   val map_cong_of_bnf: bnf -> thm
   val map_def_of_bnf: bnf -> thm
+  val map_id0_of_bnf: bnf -> thm
   val map_id'_of_bnf: bnf -> thm
-  val map_id_of_bnf: bnf -> thm
   val map_transfer_of_bnf: bnf -> thm
   val map_wppull_of_bnf: bnf -> thm
   val map_wpull_of_bnf: bnf -> thm
@@ -113,7 +113,7 @@
 val fundef_cong_attrs = @{attributes [fundef_cong]};
 
 type axioms = {
-  map_id: thm,
+  map_id0: thm,
   map_comp: thm,
   map_cong0: thm,
   set_map: thm list,
@@ -125,7 +125,7 @@
 };
 
 fun mk_axioms' ((((((((id, comp), cong), nat), c_o), cinf), set_bd), wpull), rel) =
-  {map_id = id, map_comp = comp, map_cong0 = cong, set_map = nat, bd_card_order = c_o,
+  {map_id0 = id, map_comp = comp, map_cong0 = cong, set_map = nat, bd_card_order = c_o,
    bd_cinfinite = cinf, set_bd = set_bd, map_wpull = wpull, rel_OO_Grp = rel};
 
 fun dest_cons [] = raise List.Empty
@@ -147,14 +147,14 @@
 fun zip_axioms mid mcomp mcong snat bdco bdinf sbd wpull rel =
   [mid, mcomp, mcong] @ snat @ [bdco, bdinf] @ sbd @ [wpull, rel];
 
-fun dest_axioms {map_id, map_comp, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd,
+fun dest_axioms {map_id0, map_comp, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd,
   map_wpull, rel_OO_Grp} =
-  zip_axioms map_id map_comp map_cong0 set_map bd_card_order bd_cinfinite set_bd map_wpull
+  zip_axioms map_id0 map_comp map_cong0 set_map bd_card_order bd_cinfinite set_bd map_wpull
     rel_OO_Grp;
 
-fun map_axioms f {map_id, map_comp, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd,
+fun map_axioms f {map_id0, map_comp, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd,
   map_wpull, rel_OO_Grp} =
-  {map_id = f map_id,
+  {map_id0 = f map_id0,
     map_comp = f map_comp,
     map_cong0 = f map_cong0,
     set_map = map f set_map,
@@ -380,7 +380,7 @@
 val in_mono_of_bnf = Lazy.force o #in_mono o #facts o rep_bnf;
 val in_rel_of_bnf = Lazy.force o #in_rel o #facts o rep_bnf;
 val map_def_of_bnf = #map_def o #defs o rep_bnf;
-val map_id_of_bnf = #map_id o #axioms o rep_bnf;
+val map_id0_of_bnf = #map_id0 o #axioms o rep_bnf;
 val map_id'_of_bnf = Lazy.force o #map_id' o #facts o rep_bnf;
 val map_comp_of_bnf = #map_comp o #axioms o rep_bnf;
 val map_comp'_of_bnf = Lazy.force o #map_comp' o #facts o rep_bnf;
@@ -508,7 +508,7 @@
 val in_bdN = "in_bd";
 val in_monoN = "in_mono";
 val in_relN = "in_rel";
-val map_idN = "map_id";
+val map_id0N = "map_id0";
 val map_id'N = "map_id'";
 val map_compN = "map_comp";
 val map_comp'N = "map_comp'";
@@ -559,7 +559,7 @@
             (in_monoN, [Lazy.force (#in_mono facts)]),
             (in_relN, [Lazy.force (#in_rel facts)]),
             (map_compN, [#map_comp axioms]),
-            (map_idN, [#map_id axioms]),
+            (map_id0N, [#map_id0 axioms]),
             (map_transferN, [Lazy.force (#map_transfer facts)]),
             (map_wpullN, [#map_wpull axioms]),
             (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)]),
@@ -845,7 +845,7 @@
       | defs => Proof_Display.print_consts true lthy_old (K false)
           (map (dest_Free o fst o Logic.dest_equals o prop_of) defs);
 
-    val map_id_goal =
+    val map_id0_goal =
       let val bnf_map_app_id = Term.list_comb (bnf_map_AsAs, map HOLogic.id_const As') in
         mk_Trueprop_eq (bnf_map_app_id, HOLogic.id_const CA')
       end;
@@ -922,8 +922,8 @@
 
     val rel_OO_Grp_goal = fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (rel, Rs), OO_Grp));
 
-    val goals = zip_axioms map_id_goal map_comp_goal map_cong0_goal set_maps_goal card_order_bd_goal
-      cinfinite_bd_goal set_bds_goal map_wpull_goal rel_OO_Grp_goal;
+    val goals = zip_axioms map_id0_goal map_comp_goal map_cong0_goal set_maps_goal
+      card_order_bd_goal cinfinite_bd_goal set_bds_goal map_wpull_goal rel_OO_Grp_goal;
 
     fun mk_wit_goals (I, wit) =
       let
@@ -1000,7 +1000,7 @@
 
         val in_cong = Lazy.lazy mk_in_cong;
 
-        val map_id' = Lazy.lazy (fn () => mk_map_id' (#map_id axioms));
+        val map_id' = Lazy.lazy (fn () => mk_map_id' (#map_id0 axioms));
         val map_comp' = Lazy.lazy (fn () => mk_map_comp' (#map_comp axioms));
 
         fun mk_map_cong () =
@@ -1086,7 +1086,7 @@
                 (Logic.list_implies (prems, HOLogic.mk_Trueprop concl))
           in
             Goal.prove_sorry lthy [] [] goal
-              (fn _ => mk_map_wppull_tac (#map_id axioms) (#map_cong0 axioms)
+              (fn _ => mk_map_wppull_tac (#map_id0 axioms) (#map_cong0 axioms)
                 (#map_wpull axioms) (Lazy.force map_comp') (map Lazy.force set_map'))
             |> Thm.close_derivation
           end;
@@ -1102,7 +1102,7 @@
             val goal = fold_rev Logic.all (As @ fs) (mk_Trueprop_eq (lhs, rhs));
           in
             Goal.prove_sorry lthy [] [] goal
-              (mk_rel_Grp_tac rel_OO_Grps (#map_id axioms) (#map_cong0 axioms) (Lazy.force map_id')
+              (mk_rel_Grp_tac rel_OO_Grps (#map_id0 axioms) (#map_cong0 axioms) (Lazy.force map_id')
                 (Lazy.force map_comp') (map Lazy.force set_map'))
             |> Thm.close_derivation
           end;
@@ -1142,7 +1142,7 @@
           Goal.prove_sorry lthy [] []
             (mk_Trueprop_eq (Term.list_comb (relAsAs, map HOLogic.eq_const As'),
               HOLogic.eq_const CA'))
-            (K (mk_rel_eq_tac live (Lazy.force rel_Grp) (Lazy.force rel_cong) (#map_id axioms)))
+            (K (mk_rel_eq_tac live (Lazy.force rel_Grp) (Lazy.force rel_cong) (#map_id0 axioms)))
           |> Thm.close_derivation;
 
         val rel_eq = Lazy.lazy mk_rel_eq;

--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML	Thu Aug 29 18:31:23 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML	Thu Aug 29 18:44:03 2013 +0200
@@ -66,9 +66,9 @@
     rtac set_map) set_maps) THEN'
   rtac @{thm image_empty}) 1;
 
-fun mk_map_wppull_tac map_id map_cong0 map_wpull map_comp set_maps =
+fun mk_map_wppull_tac map_id0 map_cong0 map_wpull map_comp set_maps =
   if null set_maps then
-    EVERY' [rtac @{thm wppull_id}, rtac map_wpull, rtac map_id, rtac map_id] 1
+    EVERY' [rtac @{thm wppull_id}, rtac map_wpull, rtac map_id0, rtac map_id0] 1
   else EVERY' [REPEAT_DETERM o etac conjE, REPEAT_DETERM o dtac @{thm wppull_thePull},
     REPEAT_DETERM o etac exE, rtac @{thm wpull_wppull}, rtac map_wpull,
     REPEAT_DETERM o rtac @{thm wpull_thePull}, rtac ballI,
@@ -82,14 +82,14 @@
         rtac (o_apply RS trans RS sym), rtac (o_apply RS trans), rtac thm,
         rtac conjunct2, etac bspec, etac set_mp, atac]]) [conjunct1, conjunct2]] 1;
 
-fun mk_rel_Grp_tac rel_OO_Grps map_id map_cong0 map_id' map_comp set_maps
+fun mk_rel_Grp_tac rel_OO_Grps map_id0 map_cong0 map_id' map_comp set_maps
   {context = ctxt, prems = _} =
   let
     val n = length set_maps;
     val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac else rtac (hd rel_OO_Grps RS trans);
   in
     if null set_maps then
-      unfold_thms_tac ctxt ((map_id RS @{thm Grp_UNIV_id}) :: rel_OO_Grps) THEN
+      unfold_thms_tac ctxt ((map_id0 RS @{thm Grp_UNIV_id}) :: rel_OO_Grps) THEN
       rtac @{thm Grp_UNIV_idI[OF refl]} 1
     else
       EVERY' [rel_OO_Grps_tac, rtac @{thm antisym}, rtac @{thm predicate2I},
@@ -104,8 +104,8 @@
         rtac @{thm predicate2I}, REPEAT_DETERM o eresolve_tac [@{thm GrpE}, exE, conjE],
         hyp_subst_tac ctxt,
         rtac @{thm relcomppI}, rtac @{thm conversepI},
-        EVERY' (map2 (fn convol => fn map_id =>
-          EVERY' [rtac @{thm GrpI}, rtac (box_equals OF [map_cong0, map_comp RS sym, map_id]),
+        EVERY' (map2 (fn convol => fn map_id0 =>
+          EVERY' [rtac @{thm GrpI}, rtac (box_equals OF [map_cong0, map_comp RS sym, map_id0]),
             REPEAT_DETERM_N n o rtac (convol RS fun_cong),
             REPEAT_DETERM o eresolve_tac [CollectE, conjE],
             rtac CollectI,
@@ -116,13 +116,13 @@
           @{thms fst_convol snd_convol} [map_id', refl])] 1
   end;
 
-fun mk_rel_eq_tac n rel_Grp rel_cong map_id =
+fun mk_rel_eq_tac n rel_Grp rel_cong map_id0 =
   (EVERY' (rtac (rel_cong RS trans) :: replicate n (rtac @{thm eq_alt})) THEN'
   rtac (rel_Grp RSN (2, @{thm box_equals[OF _ sym sym[OF eq_alt]]})) THEN'
   (if n = 0 then rtac refl
   else EVERY' [rtac @{thm arg_cong2[of _ _ _ _ "Grp"]},
     rtac @{thm equalityI}, rtac subset_UNIV, rtac subsetI, rtac CollectI,
-    CONJ_WRAP' (K (rtac subset_UNIV)) (1 upto n), rtac map_id])) 1;
+    CONJ_WRAP' (K (rtac subset_UNIV)) (1 upto n), rtac map_id0])) 1;
 
 fun mk_rel_mono_tac rel_OO_Grps in_mono =
   let

--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Aug 29 18:31:23 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Aug 29 18:44:03 2013 +0200
@@ -602,8 +602,8 @@
 
     val pre_map_defs = map map_def_of_bnf pre_bnfs;
     val pre_set_defss = map set_defs_of_bnf pre_bnfs;
-    val nesting_map_ids'' = map (unfold_thms lthy [id_def] o map_id_of_bnf) nesting_bnfs;
-    val nested_map_ids'' = map (unfold_thms lthy [id_def] o map_id_of_bnf) nested_bnfs;
+    val nesting_map_ids'' = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs;
+    val nested_map_ids'' = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs;
     val nested_set_map's = maps set_map'_of_bnf nested_bnfs;
 
     val fp_b_names = map base_name_of_typ fpTs;
@@ -763,7 +763,7 @@
 
     val pre_map_defs = map map_def_of_bnf pre_bnfs;
     val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
-    val nesting_map_ids'' = map (unfold_thms lthy [id_def] o map_id_of_bnf) nesting_bnfs;
+    val nesting_map_ids'' = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs;
     val nesting_rel_eqs = map rel_eq_of_bnf nesting_bnfs;
 
     val fp_b_names = map base_name_of_typ fpTs;

--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Thu Aug 29 18:31:23 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Thu Aug 29 18:44:03 2013 +0200
@@ -218,7 +218,7 @@
     val sym_map_comps = map mk_sym map_comps;
     val map_comp's = map map_comp'_of_bnf bnfs;
     val map_cong0s = map map_cong0_of_bnf bnfs;
-    val map_ids = map map_id_of_bnf bnfs;
+    val map_id0s = map map_id0_of_bnf bnfs;
     val map_id's = map map_id'_of_bnf bnfs;
     val map_wpulls = map map_wpull_of_bnf bnfs;
     val set_bdss = map set_bd_of_bnf bnfs;
@@ -2007,7 +2007,7 @@
       `split_conj_thm (split_conj_prems n
         (mor_UNIV_thm RS iffD2 RS corec_unique_mor_thm)
         |> Local_Defs.unfold lthy (@{thms o_sum_case o_id id_o o_assoc sum_case_o_inj(1)} @
-           map_ids @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ sum_case, OF refl]});
+           map_id0s @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ sum_case, OF refl]});
 
     val timer = time (timer "corec definitions & thms");
 
@@ -2074,8 +2074,8 @@
 
     val timer = time (timer "coinduction");
 
-    fun mk_dtor_map_DEADID_thm dtor_inject map_id =
-      trans OF [iffD2 OF [dtor_inject, id_apply], map_id RS sym];
+    fun mk_dtor_map_DEADID_thm dtor_inject map_id0 =
+      trans OF [iffD2 OF [dtor_inject, id_apply], map_id0 RS sym];
 
     fun mk_dtor_Jrel_DEADID_thm dtor_inject bnf =
       trans OF [rel_eq_of_bnf bnf RS @{thm predicate2_eqD}, dtor_inject] RS sym;
@@ -2457,8 +2457,8 @@
 
         val timer = time (timer "helpers for BNF properties");
 
-        val map_id_tacs =
-          map2 (K oo mk_map_id_tac map_thms) dtor_unfold_unique_thms unfold_dtor_thms;
+        val map_id0_tacs =
+          map2 (K oo mk_map_id0_tac map_thms) dtor_unfold_unique_thms unfold_dtor_thms;
         val map_comp_tacs = map (fn thm => K (rtac (thm RS sym) 1)) map_comp_thms;
         val map_cong0_tacs = map (mk_map_cong0_tac m) map_cong0_thms;
         val set_nat_tacss =
@@ -2476,7 +2476,7 @@
 
         val rel_OO_Grp_tacs = replicate n (K (rtac refl 1));
 
-        val tacss = map9 zip_axioms map_id_tacs map_comp_tacs map_cong0_tacs set_nat_tacss
+        val tacss = map9 zip_axioms map_id0_tacs map_comp_tacs map_cong0_tacs set_nat_tacss
           bd_co_tacs bd_cinf_tacs set_bd_tacss map_wpull_tacs rel_OO_Grp_tacs;
 
         val (hset_dtor_incl_thmss, hset_hset_dtor_incl_thmsss, dtor_hset_induct_thms) =

--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Thu Aug 29 18:31:23 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Thu Aug 29 18:44:03 2013 +0200
@@ -55,7 +55,7 @@
   val mk_map_comp_tac: int -> int -> thm list -> thm list -> thm list -> thm -> tactic
   val mk_mcong_tac: Proof.context -> int -> (int -> tactic) -> thm list -> thm list -> thm list ->
     thm list list -> thm list list -> thm list list list -> tactic
-  val mk_map_id_tac: thm list -> thm -> thm -> tactic
+  val mk_map_id0_tac: thm list -> thm -> thm -> tactic
   val mk_map_tac: int -> int -> ctyp option -> thm -> thm -> thm -> tactic
   val mk_dtor_map_unique_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
   val mk_mor_Abs_tac: thm list -> thm list -> {prems: 'a, context: Proof.context} -> tactic
@@ -1030,7 +1030,7 @@
     REPEAT_DETERM_N (n - 1) o rtac @{thm Un_least},
     EVERY' (map (fn thm => rtac @{thm UN_least} THEN' etac thm) set_hset_incl_hsets)] 1;
 
-fun mk_map_id_tac maps unfold_unique unfold_dtor =
+fun mk_map_id0_tac maps unfold_unique unfold_dtor =
   EVERY' [rtac (unfold_unique RS trans), EVERY' (map (rtac o mk_sym) maps),
     rtac unfold_dtor] 1;
 

--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Thu Aug 29 18:31:23 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Thu Aug 29 18:44:03 2013 +0200
@@ -162,7 +162,7 @@
     val sym_map_comps = map (fn bnf => map_comp_of_bnf bnf RS sym) bnfs;
     val map_comp's = map map_comp'_of_bnf bnfs;
     val map_cong0s = map map_cong0_of_bnf bnfs;
-    val map_ids = map map_id_of_bnf bnfs;
+    val map_id0s = map map_id0_of_bnf bnfs;
     val map_id's = map map_id'_of_bnf bnfs;
     val map_wpulls = map map_wpull_of_bnf bnfs;
     val set_map'ss = map set_map'_of_bnf bnfs;
@@ -1303,7 +1303,7 @@
       `split_conj_thm (split_conj_prems n
         (mor_UNIV_thm RS iffD2 RS rec_unique_mor_thm)
         |> Local_Defs.unfold lthy (@{thms convol_o o_id id_o o_assoc[symmetric] fst_convol} @
-           map_ids @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ convol, OF refl]});
+           map_id0s @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ convol, OF refl]});
 
     val timer = time (timer "rec definitions & thms");
 
@@ -1385,8 +1385,8 @@
 
     val timer = time (timer "induction");
 
-    fun mk_ctor_map_DEADID_thm ctor_inject map_id =
-      trans OF [id_apply, iffD2 OF [ctor_inject, map_id RS sym]];
+    fun mk_ctor_map_DEADID_thm ctor_inject map_id0 =
+      trans OF [id_apply, iffD2 OF [ctor_inject, map_id0 RS sym]];
 
     fun mk_ctor_Irel_DEADID_thm ctor_inject bnf =
       trans OF [ctor_inject, rel_eq_of_bnf bnf RS @{thm predicate2_eqD} RS sym];
@@ -1691,7 +1691,7 @@
 
         val timer = time (timer "helpers for BNF properties");
 
-        val map_id_tacs = map (K o mk_map_id_tac map_ids) ctor_map_unique_thms;
+        val map_id0_tacs = map (K o mk_map_id0_tac map_id0s) ctor_map_unique_thms;
         val map_comp_tacs =
           map2 (K oo mk_map_comp_tac map_comp's ctor_map_thms) ctor_map_unique_thms ks;
         val map_cong0_tacs = map (mk_map_cong0_tac m) map_cong0_thms;
@@ -1703,7 +1703,7 @@
 
         val rel_OO_Grp_tacs = replicate n (K (rtac refl 1));
 
-        val tacss = map9 zip_axioms map_id_tacs map_comp_tacs map_cong0_tacs set_nat_tacss
+        val tacss = map9 zip_axioms map_id0_tacs map_comp_tacs map_cong0_tacs set_nat_tacss
           bd_co_tacs bd_cinf_tacs set_bd_tacss map_wpull_tacs rel_OO_Grp_tacs;
 
         val ctor_witss =

--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Thu Aug 29 18:31:23 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Thu Aug 29 18:44:03 2013 +0200
@@ -40,7 +40,7 @@
   val mk_lfp_map_wpull_tac: Proof.context -> int -> (int -> tactic) -> thm list -> thm list ->
     thm list list -> thm list list list -> thm list -> tactic
   val mk_map_comp_tac: thm list -> thm list -> thm -> int -> tactic
-  val mk_map_id_tac: thm list -> thm -> tactic
+  val mk_map_id0_tac: thm list -> thm -> tactic
   val mk_map_tac: int -> int -> thm -> thm -> thm -> tactic
   val mk_ctor_map_unique_tac: thm -> thm list -> {prems: thm list, context: Proof.context} -> tactic
   val mk_mcong_tac: (int -> tactic) -> thm list list list -> thm list -> thm list ->
@@ -704,11 +704,11 @@
 
 (* BNF tactics *)
 
-fun mk_map_id_tac map_ids unique =
+fun mk_map_id0_tac map_id0s unique =
   (rtac sym THEN' rtac unique THEN'
   EVERY' (map (fn thm =>
     EVERY' [rtac trans, rtac @{thm id_o}, rtac trans, rtac sym, rtac @{thm o_id},
-      rtac (thm RS sym RS arg_cong)]) map_ids)) 1;
+      rtac (thm RS sym RS arg_cong)]) map_id0s)) 1;
 
 fun mk_map_comp_tac map_comps ctor_maps unique iplus1 =
   let