# HG changeset patch
# User blanchet
# Date 1377808786 -7200
# Node ID 271b34513bfbbde3d744ae029079b9f1b5561fb2
# Parent  7422380afe235e26dda85c9f16862ef563d629d3
renamed BNF axiom

diff -r 7422380afe23 -r 271b34513bfb src/HOL/BNF/Tools/bnf_comp.ML
--- a/src/HOL/BNF/Tools/bnf_comp.ML	Thu Aug 29 22:39:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML	Thu Aug 29 22:39:46 2013 +0200
@@ -153,12 +153,12 @@
       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)
-        (map map_comp_of_bnf inners);
+    fun map_comp0_tac _ =
+      mk_comp_map_comp0_tac (map_comp0_of_bnf outer) (map_cong0_of_bnf outer)
+        (map map_comp0_of_bnf inners);
 
     fun mk_single_set_map_tac i _ =
-      mk_comp_set_map_tac (map_comp_of_bnf outer) (map_cong0_of_bnf outer)
+      mk_comp_set_map_tac (map_comp0_of_bnf outer) (map_cong0_of_bnf outer)
         (collect_set_map_of_bnf outer)
         (map ((fn thms => nth thms i) o set_map_of_bnf) inners);
 
@@ -233,7 +233,7 @@
         rtac thm 1
       end;
 
-    val tacs = zip_axioms map_id0_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
+    val tacs = zip_axioms map_id0_tac map_comp0_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;
@@ -301,8 +301,8 @@
       (Library.foldr1 (uncurry mk_csum) (map (mk_card_of o HOLogic.mk_UNIV) killedAs)) bnf_bd;
 
     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
+    fun map_comp0_tac {context = ctxt, prems = _} =
+      unfold_thms_tac ctxt (map_comp0_of_bnf bnf RS sym :: @{thms o_assoc id_o o_id}) THEN
       rtac refl 1;
     fun map_cong0_tac {context = ctxt, prems = _} =
       mk_kill_map_cong0_tac ctxt n (live - n) (map_cong0_of_bnf bnf);
@@ -339,7 +339,7 @@
         rtac thm 1
       end;
 
-    val tacs = zip_axioms map_id0_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
+    val tacs = zip_axioms map_id0_tac map_comp0_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;
@@ -391,8 +391,8 @@
     val bd = mk_bd_of_bnf Ds As bnf;
 
     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
+    fun map_comp0_tac {context = ctxt, prems = _} =
+      unfold_thms_tac ctxt (map_comp0_of_bnf bnf RS sym :: @{thms o_assoc id_o o_id}) THEN
       rtac refl 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);
@@ -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_id0_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
+    val tacs = zip_axioms map_id0_tac map_comp0_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);
@@ -475,7 +475,7 @@
     val bd = mk_bd_of_bnf Ds As bnf;
 
     fun map_id0_tac _ = rtac (map_id0_of_bnf bnf) 1;
-    fun map_comp_tac _ = rtac (map_comp_of_bnf bnf) 1;
+    fun map_comp0_tac _ = rtac (map_comp0_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);
     val set_map_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_map_of_bnf bnf));
@@ -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_id0_tac map_comp_tac map_cong0_tac set_map_tacs bd_card_order_tac
+    val tacs = zip_axioms map_id0_tac map_comp0_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_id0_of_bnf bnf)) (mk_tac (map_comp_of_bnf bnf))
+    val tacs = zip_axioms (mk_tac (map_id0_of_bnf bnf)) (mk_tac (map_comp0_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))
diff -r 7422380afe23 -r 271b34513bfb src/HOL/BNF/Tools/bnf_comp_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML	Thu Aug 29 22:39:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML	Thu Aug 29 22:39:46 2013 +0200
@@ -11,7 +11,7 @@
   val mk_comp_bd_card_order_tac: thm list -> thm -> tactic
   val mk_comp_bd_cinfinite_tac: thm -> thm -> tactic
   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_comp0_tac: thm -> thm -> thm list -> tactic
   val mk_comp_map_cong0_tac: thm list -> 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
@@ -62,17 +62,17 @@
   EVERY' ([rtac ext, rtac (Gmap_cong0 RS trans)] @
     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 =
+fun mk_comp_map_comp0_tac Gmap_comp0 Gmap_cong0 map_comp0s =
   EVERY' ([rtac ext, rtac sym, rtac trans_o_apply,
-    rtac (Gmap_comp RS sym RS o_eq_dest_lhs RS trans), rtac Gmap_cong0] @
-    map (fn thm => rtac (thm RS sym RS fun_cong)) map_comps) 1;
+    rtac (Gmap_comp0 RS sym RS o_eq_dest_lhs RS trans), rtac Gmap_cong0] @
+    map (fn thm => rtac (thm RS sym RS fun_cong)) map_comp0s) 1;
 
-fun mk_comp_set_map_tac Gmap_comp Gmap_cong0 Gset_map set_maps =
+fun mk_comp_set_map_tac Gmap_comp0 Gmap_cong0 Gset_map set_maps =
   EVERY' ([rtac ext] @
     replicate 3 (rtac trans_o_apply) @
     [rtac (arg_cong_Union RS trans),
      rtac (@{thm arg_cong2[of _ _ _ _ collect, OF refl]} RS trans),
-     rtac (Gmap_comp RS sym RS o_eq_dest_lhs RS trans),
+     rtac (Gmap_comp0 RS sym RS o_eq_dest_lhs RS trans),
      rtac Gmap_cong0] @
      map (fn thm => rtac (thm RS fun_cong)) set_maps @
      [rtac (Gset_map RS o_eq_dest_lhs), rtac sym, rtac trans_o_apply,
diff -r 7422380afe23 -r 271b34513bfb src/HOL/BNF/Tools/bnf_def.ML
--- a/src/HOL/BNF/Tools/bnf_def.ML	Thu Aug 29 22:39:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Thu Aug 29 22:39:46 2013 +0200
@@ -51,7 +51,7 @@
   val in_mono_of_bnf: bnf -> thm
   val in_rel_of_bnf: bnf -> thm
   val map_comp'_of_bnf: bnf -> thm
-  val map_comp_of_bnf: bnf -> thm
+  val map_comp0_of_bnf: bnf -> thm
   val map_cong0_of_bnf: bnf -> thm
   val map_cong_of_bnf: bnf -> thm
   val map_def_of_bnf: bnf -> thm
@@ -114,7 +114,7 @@
 
 type axioms = {
   map_id0: thm,
-  map_comp: thm,
+  map_comp0: thm,
   map_cong0: thm,
   set_map: thm list,
   bd_card_order: thm,
@@ -125,7 +125,7 @@
 };
 
 fun mk_axioms' ((((((((id, comp), cong), nat), c_o), cinf), set_bd), wpull), rel) =
-  {map_id0 = id, map_comp = comp, map_cong0 = cong, set_map = nat, bd_card_order = c_o,
+  {map_id0 = id, map_comp0 = 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,15 +147,15 @@
 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_id0, map_comp, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd,
+fun dest_axioms {map_id0, map_comp0, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd,
   map_wpull, rel_OO_Grp} =
-  zip_axioms map_id0 map_comp map_cong0 set_map bd_card_order bd_cinfinite set_bd map_wpull
+  zip_axioms map_id0 map_comp0 map_cong0 set_map bd_card_order bd_cinfinite set_bd map_wpull
     rel_OO_Grp;
 
-fun map_axioms f {map_id0, map_comp, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd,
+fun map_axioms f {map_id0, map_comp0, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd,
   map_wpull, rel_OO_Grp} =
   {map_id0 = f map_id0,
-    map_comp = f map_comp,
+    map_comp0 = f map_comp0,
     map_cong0 = f map_cong0,
     set_map = map f set_map,
     bd_card_order = f bd_card_order,
@@ -382,7 +382,7 @@
 val map_def_of_bnf = #map_def o #defs 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_comp0_of_bnf = #map_comp0 o #axioms o rep_bnf;
 val map_comp'_of_bnf = Lazy.force o #map_comp' o #facts o rep_bnf;
 val map_cong0_of_bnf = #map_cong0 o #axioms o rep_bnf;
 val map_cong_of_bnf = Lazy.force o #map_cong o #facts o rep_bnf;
@@ -510,7 +510,7 @@
 val in_relN = "in_rel";
 val map_id0N = "map_id0";
 val map_idN = "map_id";
-val map_compN = "map_comp";
+val map_comp0N = "map_comp0";
 val map_comp'N = "map_comp'";
 val map_cong0N = "map_cong0";
 val map_congN = "map_cong";
@@ -558,7 +558,7 @@
             (in_bdN, [Lazy.force (#in_bd facts)]),
             (in_monoN, [Lazy.force (#in_mono facts)]),
             (in_relN, [Lazy.force (#in_rel facts)]),
-            (map_compN, [#map_comp axioms]),
+            (map_comp0N, [#map_comp0 axioms]),
             (map_id0N, [#map_id0 axioms]),
             (map_transferN, [Lazy.force (#map_transfer facts)]),
             (map_wpullN, [#map_wpull axioms]),
@@ -850,7 +850,7 @@
         mk_Trueprop_eq (bnf_map_app_id, HOLogic.id_const CA')
       end;
 
-    val map_comp_goal =
+    val map_comp0_goal =
       let
         val bnf_map_app_comp = Term.list_comb (bnf_map_AsCs, map2 (curry HOLogic.mk_comp) gs fs);
         val comp_bnf_map_app = HOLogic.mk_comp
@@ -922,7 +922,7 @@
 
     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_id0_goal map_comp_goal map_cong0_goal set_maps_goal
+    val goals = zip_axioms map_id0_goal map_comp0_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) =
@@ -1001,7 +1001,7 @@
         val in_cong = Lazy.lazy mk_in_cong;
 
         val map_id = Lazy.lazy (fn () => mk_map_id (#map_id0 axioms));
-        val map_comp' = Lazy.lazy (fn () => mk_map_comp' (#map_comp axioms));
+        val map_comp' = Lazy.lazy (fn () => mk_map_comp' (#map_comp0 axioms));
 
         fun mk_map_cong () =
           let
diff -r 7422380afe23 -r 271b34513bfb src/HOL/BNF/Tools/bnf_def_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML	Thu Aug 29 22:39:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML	Thu Aug 29 22:39:46 2013 +0200
@@ -66,7 +66,7 @@
     rtac set_map) set_maps) THEN'
   rtac @{thm image_empty}) 1;
 
-fun mk_map_wppull_tac map_id0 map_cong0 map_wpull map_comp set_maps =
+fun mk_map_wppull_tac map_id0 map_cong0 map_wpull map_comp0 set_maps =
   if null set_maps then
     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},
@@ -76,13 +76,13 @@
     CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans),
       rtac @{thm image_subsetI}, rtac conjunct1, etac bspec, etac set_mp, atac])
       set_maps,
-    CONJ_WRAP' (fn thm => EVERY' [rtac (map_comp RS trans), rtac (map_comp RS trans),
-      rtac (map_comp RS trans RS sym), rtac map_cong0,
+    CONJ_WRAP' (fn thm => EVERY' [rtac (map_comp0 RS trans), rtac (map_comp0 RS trans),
+      rtac (map_comp0 RS trans RS sym), rtac map_cong0,
       REPEAT_DETERM_N (length set_maps) o EVERY' [rtac (o_apply RS trans),
         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_id0 map_cong0 map_id map_comp set_maps
+fun mk_rel_Grp_tac rel_OO_Grps map_id0 map_cong0 map_id map_comp0 set_maps
   {context = ctxt, prems = _} =
   let
     val n = length set_maps;
@@ -95,7 +95,7 @@
       EVERY' [rel_OO_Grps_tac, rtac @{thm antisym}, rtac @{thm predicate2I},
         REPEAT_DETERM o
           eresolve_tac [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}],
-        hyp_subst_tac ctxt, rtac @{thm GrpI}, rtac trans, rtac map_comp, rtac map_cong0,
+        hyp_subst_tac ctxt, rtac @{thm GrpI}, rtac trans, rtac map_comp0, rtac map_cong0,
         REPEAT_DETERM_N n o EVERY' [rtac @{thm Collect_split_Grp_eqD}, etac @{thm set_mp}, atac],
         rtac CollectI,
         CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans),
@@ -105,7 +105,7 @@
         hyp_subst_tac ctxt,
         rtac @{thm relcomppI}, rtac @{thm conversepI},
         EVERY' (map2 (fn convol => fn map_id0 =>
-          EVERY' [rtac @{thm GrpI}, rtac (box_equals OF [map_cong0, map_comp RS sym, map_id0]),
+          EVERY' [rtac @{thm GrpI}, rtac (box_equals OF [map_cong0, map_comp0 RS sym, map_id0]),
             REPEAT_DETERM_N n o rtac (convol RS fun_cong),
             REPEAT_DETERM o eresolve_tac [CollectE, conjE],
             rtac CollectI,
@@ -135,7 +135,7 @@
       rtac @{thm Grp_mono}, rtac in_mono, REPEAT_DETERM o etac @{thm Collect_split_mono}] 1
   end;
 
-fun mk_rel_conversep_le_tac rel_OO_Grps rel_eq map_cong0 map_comp set_maps
+fun mk_rel_conversep_le_tac rel_OO_Grps rel_eq map_cong0 map_comp0 set_maps
   {context = ctxt, prems = _} =
   let
     val n = length set_maps;
@@ -151,7 +151,7 @@
         hyp_subst_tac ctxt, rtac @{thm conversepI}, rtac @{thm relcomppI}, rtac @{thm conversepI},
         EVERY' (map (fn thm => EVERY' [rtac @{thm GrpI}, rtac sym, rtac trans,
           rtac map_cong0, REPEAT_DETERM_N n o rtac thm,
-          rtac (map_comp RS sym), rtac CollectI,
+          rtac (map_comp0 RS sym), rtac CollectI,
           CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans),
             etac @{thm flip_pred}]) set_maps]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1
   end;
@@ -161,7 +161,7 @@
     rtac le_conversep, rtac @{thm iffD2[OF conversep_mono]}, rtac rel_mono,
     REPEAT_DETERM o rtac @{thm eq_refl[OF sym[OF conversep_conversep]]}] 1;
 
-fun mk_rel_OO_tac rel_OO_Grps rel_eq map_cong0 map_wppull map_comp set_maps
+fun mk_rel_OO_tac rel_OO_Grps rel_eq map_cong0 map_wppull map_comp0 set_maps
   {context = ctxt, prems = _} =
   let
     val n = length set_maps;
@@ -180,20 +180,20 @@
           eresolve_tac [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}],
         hyp_subst_tac ctxt,
         rtac @{thm relcomppI}, rtac @{thm relcomppI}, rtac @{thm conversepI}, rtac @{thm GrpI},
-        rtac trans, rtac map_comp, rtac sym, rtac map_cong0,
+        rtac trans, rtac map_comp0, rtac sym, rtac map_cong0,
         REPEAT_DETERM_N n o rtac @{thm fst_fstOp},
         in_tac @{thm fstOp_in},
-        rtac @{thm GrpI}, rtac trans, rtac map_comp, rtac map_cong0,
+        rtac @{thm GrpI}, rtac trans, rtac map_comp0, rtac map_cong0,
         REPEAT_DETERM_N n o EVERY' [rtac trans, rtac o_apply, 
           rtac ballE, rtac subst,
           rtac @{thm csquare_def}, rtac @{thm csquare_fstOp_sndOp}, atac, etac notE,
           etac set_mp, atac],
         in_tac @{thm fstOp_in},
         rtac @{thm relcomppI}, rtac @{thm conversepI}, rtac @{thm GrpI},
-        rtac trans, rtac map_comp, rtac map_cong0,
+        rtac trans, rtac map_comp0, rtac map_cong0,
         REPEAT_DETERM_N n o rtac o_apply,
         in_tac @{thm sndOp_in},
-        rtac @{thm GrpI}, rtac trans, rtac map_comp, rtac sym, rtac map_cong0,
+        rtac @{thm GrpI}, rtac trans, rtac map_comp0, rtac sym, rtac map_cong0,
         REPEAT_DETERM_N n o rtac @{thm snd_sndOp},
         in_tac @{thm sndOp_in},
         rtac @{thm predicate2I},
@@ -206,7 +206,7 @@
         rtac @{thm relcomppI}, rtac @{thm conversepI},
         EVERY' (map (fn thm => EVERY' [rtac @{thm GrpI}, rtac trans,
           rtac trans, rtac map_cong0, REPEAT_DETERM_N n o rtac thm,
-          rtac (map_comp RS sym), atac, atac]) [@{thm fst_fstOp}, @{thm snd_sndOp}])] 1
+          rtac (map_comp0 RS sym), atac, atac]) [@{thm fst_fstOp}, @{thm snd_sndOp}])] 1
   end;
 
 fun mk_in_rel_tac rel_OO_Gr {context = ctxt, prems = _} =
diff -r 7422380afe23 -r 271b34513bfb src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Thu Aug 29 22:39:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Thu Aug 29 22:39:46 2013 +0200
@@ -214,8 +214,8 @@
     val bd_Cinfinites = map bd_Cinfinite_of_bnf bnfs;
     val bd_Cinfinite = hd bd_Cinfinites;
     val in_monos = map in_mono_of_bnf bnfs;
-    val map_comps = map map_comp_of_bnf bnfs;
-    val sym_map_comps = map mk_sym map_comps;
+    val map_comp0s = map map_comp0_of_bnf bnfs;
+    val sym_map_comps = map mk_sym map_comp0s;
     val map_comp's = map map_comp'_of_bnf bnfs;
     val map_cong0s = map map_cong0_of_bnf bnfs;
     val map_id0s = map map_id0_of_bnf bnfs;
@@ -237,7 +237,7 @@
 
     (*map g1 ... gm g(m+1) ... g(m+n) (map id ... id f(m+1) ... f(m+n) x) =
       map g1 ... gm (g(m+1) o f(m+1)) ... (g(m+n) o f(m+n)) x*)
-    fun mk_map_comp_id x mapAsBs mapBsCs mapAsCs map_comp =
+    fun mk_map_comp_id x mapAsBs mapBsCs mapAsCs map_comp0 =
       let
         val lhs = Term.list_comb (mapBsCs, all_gs) $
           (Term.list_comb (mapAsBs, passive_ids @ fs) $ x);
@@ -246,7 +246,7 @@
       in
         Goal.prove_sorry lthy [] []
           (fold_rev Logic.all (x :: fs @ all_gs) (mk_Trueprop_eq (lhs, rhs)))
-          (K (mk_map_comp_id_tac map_comp))
+          (K (mk_map_comp_id_tac map_comp0))
         |> Thm.close_derivation
       end;
 
@@ -2193,7 +2193,7 @@
             map_split (fn thm => (thm RS @{thm comp_eq_dest}, thm)) maps
           end;
 
-        val map_comp_thms =
+        val map_comp0_thms =
           let
             val goal = fold_rev Logic.all (fs @ gs)
               (HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
@@ -2202,7 +2202,7 @@
                 fs_maps gs_maps fgs_maps)))
           in
             split_conj_thm (Goal.prove_sorry lthy [] [] goal
-              (K (mk_map_comp_tac m n map_thms map_comps map_cong0s dtor_unfold_unique_thm))
+              (K (mk_map_comp0_tac m n map_thms map_comp0s map_cong0s dtor_unfold_unique_thm))
               |> Thm.close_derivation)
           end;
 
@@ -2459,7 +2459,7 @@
 
         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_comp0_tacs = map (fn thm => K (rtac (thm RS sym) 1)) map_comp0_thms;
         val map_cong0_tacs = map (mk_map_cong0_tac m) map_cong0_thms;
         val set_nat_tacss =
           map2 (map2 (K oo mk_set_map_tac)) hset_defss (transpose col_natural_thmss);
@@ -2476,7 +2476,7 @@
 
         val rel_OO_Grp_tacs = replicate n (K (rtac refl 1));
 
-        val tacss = map9 zip_axioms map_id0_tacs map_comp_tacs map_cong0_tacs set_nat_tacss
+        val tacss = map9 zip_axioms map_id0_tacs map_comp0_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) =
@@ -2699,11 +2699,11 @@
               (mk_Trueprop_eq (Jrelphi $ Jz $ Jz', relphi $ (dtor $ Jz) $ (dtor' $ Jz')));
             val goals = map6 mk_goal Jzs Jz's dtors dtor's Jrelphis relphis;
           in
-            map12 (fn i => fn goal => fn in_rel => fn map_comp => fn map_cong0 =>
+            map12 (fn i => fn goal => fn in_rel => fn map_comp0 => fn map_cong0 =>
               fn dtor_map => fn dtor_sets => fn dtor_inject => fn dtor_ctor =>
               fn set_maps => fn dtor_set_incls => fn dtor_set_set_inclss =>
               Goal.prove_sorry lthy [] [] goal
-                (K (mk_dtor_rel_tac lthy in_Jrels i in_rel map_comp map_cong0 dtor_map dtor_sets
+                (K (mk_dtor_rel_tac lthy in_Jrels i in_rel map_comp0 map_cong0 dtor_map dtor_sets
                   dtor_inject dtor_ctor set_maps dtor_set_incls dtor_set_set_inclss))
               |> Thm.close_derivation)
             ks goals in_rels map_comp's map_cong0s folded_dtor_map_thms folded_dtor_set_thmss'
diff -r 7422380afe23 -r 271b34513bfb src/HOL/BNF/Tools/bnf_gfp_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Thu Aug 29 22:39:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Thu Aug 29 22:39:46 2013 +0200
@@ -52,7 +52,7 @@
   val mk_incl_lsbis_tac: int -> int -> thm -> tactic
   val mk_length_Lev'_tac: thm -> tactic
   val mk_length_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> tactic
-  val mk_map_comp_tac: int -> int -> thm list -> thm list -> thm list -> thm -> tactic
+  val mk_map_comp0_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_id0_tac: thm list -> thm -> thm -> tactic
@@ -256,19 +256,19 @@
             (rev ((1 upto n) ~~ (active_set_maps ~~ coalg_sets)))])
       (rec_Sucs ~~ (morEs ~~ (map (chop m) set_mapss ~~ map (drop m) coalg_setss)))] 1;
 
-fun mk_bis_rel_tac ctxt m bis_def rel_OO_Grps map_comps map_cong0s set_mapss =
+fun mk_bis_rel_tac ctxt m bis_def rel_OO_Grps map_comp0s map_cong0s set_mapss =
   let
     val n = length rel_OO_Grps;
-    val thms = ((1 upto n) ~~ map_comps ~~ map_cong0s ~~ set_mapss ~~ rel_OO_Grps);
+    val thms = ((1 upto n) ~~ map_comp0s ~~ map_cong0s ~~ set_mapss ~~ rel_OO_Grps);
 
-    fun mk_if_tac ((((i, map_comp), map_cong0), set_maps), rel_OO_Grp) =
+    fun mk_if_tac ((((i, map_comp0), map_cong0), set_maps), rel_OO_Grp) =
       EVERY' [rtac allI, rtac allI, rtac impI, dtac (mk_conjunctN n i),
         etac allE, etac allE, etac impE, atac, etac bexE, etac conjE,
         rtac (rel_OO_Grp RS sym RS @{thm eq_refl} RS @{thm predicate2D}),
         rtac @{thm relcomppI}, rtac @{thm conversepI},
         EVERY' (map (fn thm =>
           EVERY' [rtac @{thm GrpI},
-            rtac trans, rtac trans, rtac map_comp, rtac map_cong0, REPEAT_DETERM_N m o rtac thm,
+            rtac trans, rtac trans, rtac map_comp0, rtac map_cong0, REPEAT_DETERM_N m o rtac thm,
             REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), atac,
             REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI,
             CONJ_WRAP' (fn (i, thm) =>
@@ -281,17 +281,17 @@
             (1 upto (m + n) ~~ set_maps)])
           @{thms fst_diag_id snd_diag_id})];
 
-    fun mk_only_if_tac ((((i, map_comp), map_cong0), set_maps), rel_OO_Grp) =
+    fun mk_only_if_tac ((((i, map_comp0), map_cong0), set_maps), rel_OO_Grp) =
       EVERY' [dtac (mk_conjunctN n i), rtac allI, rtac allI, rtac impI,
         etac allE, etac allE, etac impE, atac,
         dtac (rel_OO_Grp RS @{thm eq_refl} RS @{thm predicate2D}),
         REPEAT_DETERM o eresolve_tac ([CollectE, conjE, exE] @
           @{thms GrpE relcomppE conversepE CollectE Collect_split_in_rel_leE}),
         hyp_subst_tac ctxt,
-        rtac bexI, rtac conjI, rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
+        rtac bexI, rtac conjI, rtac trans, rtac map_comp0, rtac trans, rtac map_cong0,
         REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
         REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong),
-        atac, rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
+        atac, rtac trans, rtac map_comp0, rtac trans, rtac map_cong0,
         REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
         REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong),
         rtac trans, rtac map_cong0,
@@ -1034,20 +1034,20 @@
   EVERY' [rtac (unfold_unique RS trans), EVERY' (map (rtac o mk_sym) maps),
     rtac unfold_dtor] 1;
 
-fun mk_map_comp_tac m n maps map_comps map_cong0s unfold_unique =
+fun mk_map_comp0_tac m n maps map_comp0s map_cong0s unfold_unique =
   EVERY' [rtac unfold_unique,
-    EVERY' (map3 (fn map_thm => fn map_comp => fn map_cong0 =>
+    EVERY' (map3 (fn map_thm => fn map_comp0 => fn map_cong0 =>
       EVERY' (map rtac
         ([@{thm o_assoc} RS trans,
-        @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp RS sym, refl] RS trans,
+        @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp0 RS sym, refl] RS trans,
         @{thm o_assoc} RS trans RS sym,
         @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_thm, refl] RS trans,
         @{thm o_assoc} RS sym RS trans, map_thm RS arg_cong RS trans, @{thm o_assoc} RS trans,
-        @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp RS sym, refl] RS trans,
+        @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp0 RS sym, refl] RS trans,
         ext, o_apply RS trans,  o_apply RS trans RS sym, map_cong0] @
         replicate m (@{thm id_o} RS fun_cong) @
         replicate n (@{thm o_id} RS fun_cong))))
-    maps map_comps map_cong0s)] 1;
+    maps map_comp0s map_cong0s)] 1;
 
 fun mk_mcong_tac ctxt m coinduct_tac map_comp's dtor_maps map_cong0s set_mapss set_hsetss
   set_hset_hsetsss =
@@ -1177,38 +1177,38 @@
       (drop m set_maps)])
   (map_wpulls ~~ (pickWP_assms_tacs ~~ set_mapss)) 1;
 
-fun mk_mor_thePull_nth_tac conv pick m mor_def map_wpulls map_comps pickWP_assms_tacs
+fun mk_mor_thePull_nth_tac conv pick m mor_def map_wpulls map_comp0s pickWP_assms_tacs
   {context = ctxt, prems = _: thm list} =
   let
-    val n = length map_comps;
+    val n = length map_comp0s;
   in
     unfold_thms_tac ctxt [mor_def] THEN
     EVERY' [rtac conjI,
       CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) (1 upto n),
-      CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, map_comp)) =>
+      CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, map_comp0)) =>
         EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
           REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE],
           hyp_subst_tac ctxt,
           SELECT_GOAL (unfold_thms_tac ctxt @{thms o_apply prod.cases}),
-          rtac (map_comp RS trans),
+          rtac (map_comp0 RS trans),
           SELECT_GOAL (unfold_thms_tac ctxt (conv :: @{thms o_id id_o})),
           rtac (map_wpull RS pick), REPEAT_DETERM_N m o atac,
           pickWP_assms_tac])
-      (map_wpulls ~~ (pickWP_assms_tacs ~~ map_comps))] 1
+      (map_wpulls ~~ (pickWP_assms_tacs ~~ map_comp0s))] 1
   end;
 
 val mk_mor_thePull_fst_tac = mk_mor_thePull_nth_tac @{thm fst_conv} @{thm pickWP(2)};
 val mk_mor_thePull_snd_tac = mk_mor_thePull_nth_tac @{thm snd_conv} @{thm pickWP(3)};
 
-fun mk_mor_thePull_pick_tac mor_def unfolds map_comps {context = ctxt, prems = _} =
+fun mk_mor_thePull_pick_tac mor_def unfolds map_comp0s {context = ctxt, prems = _} =
   unfold_thms_tac ctxt [mor_def, @{thm thePull_def}] THEN rtac conjI 1 THEN
   CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) unfolds 1 THEN
-  CONJ_WRAP' (fn (unfold, map_comp) =>
+  CONJ_WRAP' (fn (unfold, map_comp0) =>
     EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE],
       hyp_subst_tac ctxt,
-      SELECT_GOAL (unfold_thms_tac ctxt (unfold :: map_comp :: @{thms comp_def id_def})),
+      SELECT_GOAL (unfold_thms_tac ctxt (unfold :: map_comp0 :: @{thms comp_def id_def})),
       rtac refl])
-  (unfolds ~~ map_comps) 1;
+  (unfolds ~~ map_comp0s) 1;
 
 fun mk_pick_col_tac m j cts rec_0s rec_Sucs unfolds set_mapss map_wpulls pickWP_assms_tacs
   {context = ctxt, prems = _} =
@@ -1287,7 +1287,7 @@
   ALLGOALS (TRY o
     FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE])
 
-fun mk_dtor_rel_tac ctxt in_Jrels i in_rel map_comp map_cong0 dtor_map dtor_sets dtor_inject
+fun mk_dtor_rel_tac ctxt in_Jrels i in_rel map_comp0 map_cong0 dtor_map dtor_sets dtor_inject
     dtor_ctor set_maps dtor_set_incls dtor_set_set_inclss =
   let
     val m = length dtor_set_incls;
@@ -1309,7 +1309,7 @@
             rtac conjI, rtac refl, rtac refl])
         (in_Jrels ~~ (active_set_maps ~~ dtor_set_set_inclss)),
         CONJ_WRAP' (fn conv =>
-          EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
+          EVERY' [rtac trans, rtac map_comp0, rtac trans, rtac map_cong0,
           REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
           REPEAT_DETERM_N n o EVERY' (map rtac [trans, o_apply, conv]),
           rtac trans, rtac sym, rtac dtor_map, rtac (dtor_inject RS iffD2), atac])
@@ -1339,7 +1339,7 @@
         (dtor_sets ~~ passive_set_maps),
         rtac conjI,
         REPEAT_DETERM_N 2 o EVERY'[rtac (dtor_inject RS iffD1), rtac trans, rtac dtor_map,
-          rtac box_equals, rtac map_comp, rtac (dtor_ctor RS sym RS arg_cong), rtac trans,
+          rtac box_equals, rtac map_comp0, rtac (dtor_ctor RS sym RS arg_cong), rtac trans,
           rtac map_cong0, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
           EVERY' (map (fn in_Jrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
             dtac @{thm ssubst_mem[OF pair_collapse]},
@@ -1352,22 +1352,22 @@
     EVERY' [rtac iffI, if_tac, only_if_tac] 1
   end;
 
-fun mk_rel_coinduct_coind_tac m coinduct ks map_comps map_congs map_arg_congs set_mapss 
+fun mk_rel_coinduct_coind_tac m coinduct ks map_comp0s map_congs map_arg_congs set_mapss 
   dtor_unfolds dtor_maps {context = ctxt, prems = _} =
   let val n = length ks;
   in
     EVERY' [DETERM o rtac coinduct,
-      EVERY' (map7 (fn i => fn map_comp => fn map_cong => fn map_arg_cong => fn set_maps =>
+      EVERY' (map7 (fn i => fn map_comp0 => fn map_cong => fn map_arg_cong => fn set_maps =>
           fn dtor_unfold => fn dtor_map =>
         EVERY' [REPEAT_DETERM o eresolve_tac [exE, conjE],
           select_prem_tac (length ks) (dtac @{thm spec2}) i, dtac mp, atac,
           REPEAT_DETERM o eresolve_tac [CollectE, conjE], hyp_subst_tac ctxt,
           rtac exI, rtac conjI, rtac conjI,
-          rtac (map_comp RS trans), rtac (dtor_map RS trans RS sym),
-          rtac (dtor_unfold RS map_arg_cong RS trans), rtac (trans OF [map_comp, map_cong]),
+          rtac (map_comp0 RS trans), rtac (dtor_map RS trans RS sym),
+          rtac (dtor_unfold RS map_arg_cong RS trans), rtac (trans OF [map_comp0, map_cong]),
           REPEAT_DETERM_N m o rtac @{thm trans[OF fun_cong[OF o_id] sym[OF fun_cong[OF id_o]]]},
           REPEAT_DETERM_N n o (rtac @{thm sym[OF trans[OF o_apply]]} THEN' rtac @{thm fst_conv}),
-          rtac (map_comp RS trans), rtac (map_cong RS trans),
+          rtac (map_comp0 RS trans), rtac (map_cong RS trans),
           REPEAT_DETERM_N m o rtac @{thm fun_cong[OF id_o]},
           REPEAT_DETERM_N n o (rtac @{thm trans[OF o_apply]} THEN' rtac @{thm snd_conv}),
           etac (@{thm prod.cases} RS map_arg_cong RS trans),
@@ -1380,7 +1380,7 @@
               hyp_subst_tac ctxt, rtac exI, rtac conjI, etac Collect_splitD_set_mp, atac,
               rtac (o_apply RS trans), rtac (@{thm surjective_pairing} RS arg_cong)])
           (drop m set_maps)])
-      ks map_comps map_congs map_arg_congs set_mapss dtor_unfolds dtor_maps)] 1
+      ks map_comp0s map_congs map_arg_congs set_mapss dtor_unfolds dtor_maps)] 1
   end;
 
 val split_id_unfolds = @{thms prod.cases image_id id_apply};
diff -r 7422380afe23 -r 271b34513bfb src/HOL/BNF/Tools/bnf_lfp.ML
--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Thu Aug 29 22:39:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Thu Aug 29 22:39:46 2013 +0200
@@ -159,7 +159,7 @@
         map (fn thm => ctrans OF [thm, bd0_Card_order RS @{thm ordLeq_csum1}]) set_bd0s)
       set_bd0ss bd0_Card_orders;
     val in_bds = map in_bd_of_bnf bnfs;
-    val sym_map_comps = map (fn bnf => map_comp_of_bnf bnf RS sym) bnfs;
+    val sym_map_comps = map (fn bnf => map_comp0_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_id0s = map map_id0_of_bnf bnfs;
@@ -194,7 +194,7 @@
 
     (*map g1 ... gm g(m+1) ... g(m+n) (map id ... id f(m+1) ... f(m+n) x) =
       map g1 ... gm (g(m+1) o f(m+1)) ... (g(m+n) o f(m+n)) x*)
-    fun mk_map_comp_id x mapAsBs mapBsCs mapAsCs map_comp =
+    fun mk_map_comp_id x mapAsBs mapBsCs mapAsCs map_comp0 =
       let
         val lhs = Term.list_comb (mapBsCs, all_gs) $
           (Term.list_comb (mapAsBs, passive_ids @ fs) $ x);
@@ -203,7 +203,7 @@
       in
         Goal.prove_sorry lthy [] []
           (fold_rev Logic.all (x :: fs @ all_gs) (mk_Trueprop_eq (lhs, rhs)))
-          (K (mk_map_comp_id_tac map_comp))
+          (K (mk_map_comp_id_tac map_comp0))
         |> Thm.close_derivation
       end;
 
@@ -1692,8 +1692,8 @@
         val timer = time (timer "helpers for BNF properties");
 
         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_comp0_tacs =
+          map2 (K oo mk_map_comp0_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;
         val set_nat_tacss = map (map (K o mk_set_map_tac)) (transpose set_map_thmss);
         val bd_co_tacs = replicate n (K (mk_bd_card_order_tac bd_card_orders));
@@ -1703,7 +1703,7 @@
 
         val rel_OO_Grp_tacs = replicate n (K (rtac refl 1));
 
-        val tacss = map9 zip_axioms map_id0_tacs map_comp_tacs map_cong0_tacs set_nat_tacss
+        val tacss = map9 zip_axioms map_id0_tacs map_comp0_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 =
@@ -1773,11 +1773,11 @@
               (mk_Trueprop_eq (Irelphi $ (ctor $ xF) $ (ctor' $ yF), relphi $ xF $ yF));
             val goals = map6 mk_goal xFs yFs ctors ctor's Irelphis relphis;
           in
-            map12 (fn i => fn goal => fn in_rel => fn map_comp => fn map_cong0 =>
+            map12 (fn i => fn goal => fn in_rel => fn map_comp0 => fn map_cong0 =>
               fn ctor_map => fn ctor_sets => fn ctor_inject => fn ctor_dtor =>
               fn set_maps => fn ctor_set_incls => fn ctor_set_set_inclss =>
               Goal.prove_sorry lthy [] [] goal
-               (K (mk_ctor_rel_tac lthy in_Irels i in_rel map_comp map_cong0 ctor_map ctor_sets
+               (K (mk_ctor_rel_tac lthy in_Irels i in_rel map_comp0 map_cong0 ctor_map ctor_sets
                  ctor_inject ctor_dtor set_maps ctor_set_incls ctor_set_set_inclss))
               |> Thm.close_derivation)
             ks goals in_rels map_comp's map_cong0s folded_ctor_map_thms folded_ctor_set_thmss'
diff -r 7422380afe23 -r 271b34513bfb src/HOL/BNF/Tools/bnf_lfp_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Thu Aug 29 22:39:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Thu Aug 29 22:39:46 2013 +0200
@@ -39,7 +39,7 @@
   val mk_least_min_alg_tac: thm -> thm -> tactic
   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_comp0_tac: thm list -> thm list -> thm -> int -> 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
@@ -710,11 +710,11 @@
     EVERY' [rtac trans, rtac @{thm id_o}, rtac trans, rtac sym, rtac @{thm o_id},
       rtac (thm RS sym RS arg_cong)]) map_id0s)) 1;
 
-fun mk_map_comp_tac map_comps ctor_maps unique iplus1 =
+fun mk_map_comp0_tac map_comp0s ctor_maps unique iplus1 =
   let
     val i = iplus1 - 1;
     val unique' = Thm.permute_prems 0 i unique;
-    val map_comps' = drop i map_comps @ take i map_comps;
+    val map_comps' = drop i map_comp0s @ take i map_comp0s;
     val ctor_maps' = drop i ctor_maps @ take i ctor_maps;
     fun mk_comp comp simp =
       EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, rtac o_apply,
@@ -746,7 +746,7 @@
           EVERY' [hyp_subst_tac ctxt, dtac set_rev_mp, rtac equalityD1, resolve_tac ctor_set,
             REPEAT_DETERM_N n o etac UnE]))))] 1);
 
-fun mk_ctor_rel_tac ctxt in_Irels i in_rel map_comp map_cong0 ctor_map ctor_sets ctor_inject
+fun mk_ctor_rel_tac ctxt in_Irels i in_rel map_comp0 map_cong0 ctor_map ctor_sets ctor_inject
   ctor_dtor set_maps ctor_set_incls ctor_set_set_inclss =
   let
     val m = length ctor_set_incls;
@@ -773,7 +773,7 @@
             rtac conjI, rtac refl, rtac refl])
         (in_Irels ~~ (active_set_maps ~~ ctor_set_set_inclss)),
         CONJ_WRAP' (fn conv =>
-          EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
+          EVERY' [rtac trans, rtac map_comp0, rtac trans, rtac map_cong0,
           REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
           REPEAT_DETERM_N n o EVERY' (map rtac [trans, o_apply, conv]),
           rtac (ctor_inject RS iffD1), rtac trans, rtac sym, rtac ctor_map,
@@ -802,7 +802,7 @@
         (ctor_sets ~~ passive_set_maps),
         rtac conjI,
         REPEAT_DETERM_N 2 o EVERY' [rtac trans, rtac ctor_map, rtac (ctor_inject RS iffD2),
-          rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
+          rtac trans, rtac map_comp0, rtac trans, rtac map_cong0,
           REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
           EVERY' (map (fn in_Irel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
             dtac @{thm ssubst_mem[OF pair_collapse]},
diff -r 7422380afe23 -r 271b34513bfb src/HOL/BNF/Tools/bnf_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_tactics.ML	Thu Aug 29 22:39:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_tactics.ML	Thu Aug 29 22:39:46 2013 +0200
@@ -106,8 +106,8 @@
       split_conv}) THEN
   rtac refl 1;
 
-fun mk_map_comp_id_tac map_comp =
-  (rtac trans THEN' rtac map_comp THEN' REPEAT_DETERM o stac @{thm o_id} THEN' rtac refl) 1;
+fun mk_map_comp_id_tac map_comp0 =
+  (rtac trans THEN' rtac map_comp0 THEN' REPEAT_DETERM o stac @{thm o_id} THEN' rtac refl) 1;
 
 fun mk_map_cong0_tac m map_cong0 {context = ctxt, prems = _} =
   EVERY' [rtac mp, rtac map_cong0,