# HG changeset patch
# User blanchet
# Date 1366805701 -7200
# Node ID 4c9f08836d878ea75027f36b07fc85e8cf7d5da0
# Parent  e5ce85418346a43d18a711781a792144f8d62cb1
renamed "map_cong" axiom to "map_cong0" in preparation for real "map_cong"

diff -r e5ce85418346 -r 4c9f08836d87 src/HOL/BNF/Tools/bnf_comp.ML
--- a/src/HOL/BNF/Tools/bnf_comp.ML	Wed Apr 24 14:14:36 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML	Wed Apr 24 14:15:01 2013 +0200
@@ -150,15 +150,15 @@
     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_cong_of_bnf outer)
+      mk_comp_map_id_tac (map_id_of_bnf outer) (map_cong0_of_bnf outer)
         (map map_id_of_bnf inners);
 
     fun map_comp_tac _ =
-      mk_comp_map_comp_tac (map_comp_of_bnf outer) (map_cong_of_bnf outer)
+      mk_comp_map_comp_tac (map_comp_of_bnf outer) (map_cong0_of_bnf outer)
         (map map_comp_of_bnf inners);
 
     fun mk_single_set_natural_tac i _ =
-      mk_comp_set_natural_tac (map_comp_of_bnf outer) (map_cong_of_bnf outer)
+      mk_comp_set_natural_tac (map_comp_of_bnf outer) (map_cong0_of_bnf outer)
         (collect_set_natural_of_bnf outer)
         (map ((fn thms => nth thms i) o set_natural_of_bnf) inners);
 
@@ -181,8 +181,8 @@
           |> Thm.close_derivation)
         (map2 (curry (HOLogic.mk_Trueprop o HOLogic.mk_eq)) sets sets_alt);
 
-    fun map_cong_tac _ =
-      mk_comp_map_cong_tac set_alt_thms (map_cong_of_bnf outer) (map map_cong_of_bnf inners);
+    fun map_cong0_tac _ =
+      mk_comp_map_cong0_tac set_alt_thms (map_cong0_of_bnf outer) (map map_cong0_of_bnf inners);
 
     val set_bd_tacs =
       if ! quick_and_dirty then
@@ -238,7 +238,7 @@
         unfold_thms_tac lthy basic_thms THEN rtac thm 1
       end;
 
-    val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
+    val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_natural_tacs bd_card_order_tac
       bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
 
     val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer;
@@ -309,8 +309,8 @@
     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;
-    fun map_cong_tac {context = ctxt, prems = _} =
-      mk_kill_map_cong_tac ctxt n (live - n) (map_cong_of_bnf bnf);
+    fun map_cong0_tac {context = ctxt, prems = _} =
+      mk_kill_map_cong0_tac ctxt n (live - n) (map_cong0_of_bnf bnf);
     val set_natural_tacs = map (fn thm => fn _ => rtac thm 1) (drop n (set_natural_of_bnf bnf));
     fun bd_card_order_tac _ = mk_kill_bd_card_order_tac n (bd_card_order_of_bnf bnf);
     fun bd_cinfinite_tac _ = mk_kill_bd_cinfinite_tac (bd_Cinfinite_of_bnf bnf);
@@ -348,7 +348,7 @@
         rtac thm 1
       end;
 
-    val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
+    val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_natural_tacs bd_card_order_tac
       bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
 
     val bnf_wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf;
@@ -403,8 +403,8 @@
     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;
-    fun map_cong_tac {context = ctxt, prems = _} =
-      rtac (map_cong_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 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_natural_tacs =
       if ! quick_and_dirty then
         replicate (n + live) (K all_tac)
@@ -435,7 +435,7 @@
     fun srel_O_Gr_tac _ =
       mk_simple_srel_O_Gr_tac lthy (srel_def_of_bnf bnf) (srel_O_Gr_of_bnf bnf) in_alt_thm;
 
-    val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
+    val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_natural_tacs bd_card_order_tac
       bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
 
     val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
@@ -488,8 +488,8 @@
 
     fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
     fun map_comp_tac _ = rtac (map_comp_of_bnf bnf) 1;
-    fun map_cong_tac {context = ctxt, prems = _} =
-      rtac (map_cong_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 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_natural_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_natural_of_bnf bnf));
     fun bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1;
     fun bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1;
@@ -512,7 +512,7 @@
     fun srel_O_Gr_tac _ =
       mk_simple_srel_O_Gr_tac lthy (srel_def_of_bnf bnf) (srel_O_Gr_of_bnf bnf) in_alt_thm;
 
-    val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
+    val tacs = zip_axioms map_id_tac map_comp_tac map_cong0_tac set_natural_tacs bd_card_order_tac
       bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac srel_O_Gr_tac;
 
     val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
@@ -653,7 +653,7 @@
       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))
-      (mk_tac (map_cong_of_bnf bnf)) (map mk_tac (set_natural_of_bnf bnf))
+      (mk_tac (map_cong0_of_bnf bnf)) (map mk_tac (set_natural_of_bnf bnf))
       (K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1)) (map mk_tac set_bds) (mk_tac in_bd)
       (mk_tac (map_wpull_of_bnf bnf))
       (mk_tac (unfold_thms lthy [srel_def_of_bnf bnf] (srel_O_Gr_of_bnf bnf)));
diff -r e5ce85418346 -r 4c9f08836d87 src/HOL/BNF/Tools/bnf_comp_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML	Wed Apr 24 14:14:36 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML	Wed Apr 24 14:15:01 2013 +0200
@@ -13,7 +13,7 @@
   val mk_comp_in_alt_tac: Proof.context -> thm list -> tactic
   val mk_comp_in_bd_tac: thm -> thm list -> thm -> thm list -> thm -> tactic
   val mk_comp_map_comp_tac: thm -> thm -> thm list -> tactic
-  val mk_comp_map_cong_tac: thm list -> 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_set_alt_tac: Proof.context -> thm -> tactic
   val mk_comp_set_bd_tac: Proof.context -> thm -> thm list -> tactic
@@ -24,7 +24,7 @@
   val mk_kill_bd_cinfinite_tac: thm -> tactic
   val kill_in_alt_tac: tactic
   val mk_kill_in_bd_tac: int -> bool -> thm -> thm -> thm -> thm -> thm -> tactic
-  val mk_kill_map_cong_tac: Proof.context -> int -> int -> thm -> tactic
+  val mk_kill_map_cong0_tac: Proof.context -> int -> int -> thm -> tactic
   val mk_kill_set_bd_tac: thm -> thm -> tactic
 
   val empty_natural_tac: tactic
@@ -69,22 +69,22 @@
   unfold_thms_tac ctxt [collect_set_natural RS sym] THEN
   rtac refl 1;
 
-fun mk_comp_map_id_tac Gmap_id Gmap_cong map_ids =
-  EVERY' ([rtac ext, rtac (Gmap_cong RS trans)] @
+fun mk_comp_map_id_tac Gmap_id Gmap_cong0 map_ids =
+  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;
 
-fun mk_comp_map_comp_tac Gmap_comp Gmap_cong map_comps =
+fun mk_comp_map_comp_tac Gmap_comp Gmap_cong0 map_comps =
   EVERY' ([rtac ext, rtac sym, rtac trans_o_apply,
-    rtac (Gmap_comp RS sym RS o_eq_dest_lhs RS trans), rtac Gmap_cong] @
+    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;
 
-fun mk_comp_set_natural_tac Gmap_comp Gmap_cong Gset_natural set_naturals =
+fun mk_comp_set_natural_tac Gmap_comp Gmap_cong0 Gset_natural set_naturals =
   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_cong] @
+     rtac Gmap_cong0] @
      map (fn thm => rtac (thm RS fun_cong)) set_naturals @
      [rtac (Gset_natural RS o_eq_dest_lhs), rtac sym, rtac trans_o_apply,
      rtac trans_image_cong_o_apply, rtac trans_image_cong_o_apply,
@@ -98,14 +98,14 @@
         rtac @{thm sym[OF trans[OF o_apply]]}, rtac @{thm image_cong[OF refl o_apply]}],
      rtac @{thm image_empty}]) 1;
 
-fun mk_comp_map_cong_tac comp_set_alts map_cong map_congs =
+fun mk_comp_map_cong0_tac comp_set_alts map_cong0 map_cong0s =
   let
      val n = length comp_set_alts;
   in
     (if n = 0 then rtac refl 1
-    else rtac map_cong 1 THEN
-      EVERY' (map_index (fn (i, map_cong) =>
-        rtac map_cong THEN' EVERY' (map_index (fn (k, set_alt) =>
+    else rtac map_cong0 1 THEN
+      EVERY' (map_index (fn (i, map_cong0) =>
+        rtac map_cong0 THEN' EVERY' (map_index (fn (k, set_alt) =>
           EVERY' [select_prem_tac n (dtac @{thm meta_spec}) (k + 1), etac meta_mp,
             rtac (equalityD2 RS set_mp), rtac (set_alt RS fun_cong RS trans),
             rtac trans_o_apply, rtac (@{thm collect_def} RS arg_cong_Union),
@@ -113,7 +113,7 @@
             rtac @{thm insertI1}, rtac (o_apply RS equalityD2 RS set_mp),
             etac @{thm imageI}, atac])
           comp_set_alts))
-      map_congs) 1)
+      map_cong0s) 1)
   end;
 
 fun mk_comp_bd_card_order_tac Fbd_card_orders Gbd_card_order =
@@ -233,8 +233,8 @@
 
 (* Kill operation *)
 
-fun mk_kill_map_cong_tac ctxt n m map_cong =
-  (rtac map_cong THEN' EVERY' (replicate n (rtac refl)) THEN'
+fun mk_kill_map_cong0_tac ctxt n m map_cong0 =
+  (rtac map_cong0 THEN' EVERY' (replicate n (rtac refl)) THEN'
     EVERY' (replicate m (Goal.assume_rule_tac ctxt))) 1;
 
 fun mk_kill_bd_card_order_tac n bd_card_order =
diff -r e5ce85418346 -r 4c9f08836d87 src/HOL/BNF/Tools/bnf_def.ML
--- a/src/HOL/BNF/Tools/bnf_def.ML	Wed Apr 24 14:14:36 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Wed Apr 24 14:15:01 2013 +0200
@@ -52,7 +52,7 @@
   val in_srel_of_bnf: BNF -> thm
   val map_comp'_of_bnf: BNF -> thm
   val map_comp_of_bnf: BNF -> thm
-  val map_cong_of_bnf: BNF -> thm
+  val map_cong0_of_bnf: BNF -> thm
   val map_def_of_bnf: BNF -> thm
   val map_id'_of_bnf: BNF -> thm
   val map_id_of_bnf: BNF -> thm
@@ -107,7 +107,7 @@
 type axioms = {
   map_id: thm,
   map_comp: thm,
-  map_cong: thm,
+  map_cong0: thm,
   set_natural: thm list,
   bd_card_order: thm,
   bd_cinfinite: thm,
@@ -118,7 +118,7 @@
 };
 
 fun mk_axioms' (((((((((id, comp), cong), nat), c_o), cinf), set_bd), in_bd), wpull), srel) =
-  {map_id = id, map_comp = comp, map_cong = cong, set_natural = nat, bd_card_order = c_o,
+  {map_id = id, map_comp = comp, map_cong0 = cong, set_natural = nat, bd_card_order = c_o,
    bd_cinfinite = cinf, set_bd = set_bd, in_bd = in_bd, map_wpull = wpull, srel_O_Gr = srel};
 
 fun dest_cons [] = raise Empty
@@ -141,16 +141,16 @@
 fun zip_axioms mid mcomp mcong snat bdco bdinf sbd inbd wpull srel =
   [mid, mcomp, mcong] @ snat @ [bdco, bdinf] @ sbd @ [inbd, wpull, srel];
 
-fun dest_axioms {map_id, map_comp, map_cong, set_natural, bd_card_order, bd_cinfinite, set_bd,
+fun dest_axioms {map_id, map_comp, map_cong0, set_natural, bd_card_order, bd_cinfinite, set_bd,
   in_bd, map_wpull, srel_O_Gr} =
-  zip_axioms map_id map_comp map_cong set_natural bd_card_order bd_cinfinite set_bd in_bd map_wpull
+  zip_axioms map_id map_comp map_cong0 set_natural bd_card_order bd_cinfinite set_bd in_bd map_wpull
     srel_O_Gr;
 
-fun map_axioms f {map_id, map_comp, map_cong, set_natural, bd_card_order, bd_cinfinite, set_bd,
+fun map_axioms f {map_id, map_comp, map_cong0, set_natural, bd_card_order, bd_cinfinite, set_bd,
   in_bd, map_wpull, srel_O_Gr} =
   {map_id = f map_id,
     map_comp = f map_comp,
-    map_cong = f map_cong,
+    map_cong0 = f map_cong0,
     set_natural = map f set_natural,
     bd_card_order = f bd_card_order,
     bd_cinfinite = f bd_cinfinite,
@@ -371,7 +371,7 @@
 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;
-val map_cong_of_bnf = #map_cong o #axioms o rep_bnf;
+val map_cong0_of_bnf = #map_cong0 o #axioms o rep_bnf;
 val map_wppull_of_bnf = Lazy.force o #map_wppull o #facts o rep_bnf;
 val map_wpull_of_bnf = #map_wpull o #axioms o rep_bnf;
 val rel_def_of_bnf = #rel_def o #defs o rep_bnf;
@@ -507,7 +507,7 @@
 val map_id'N = "map_id'";
 val map_compN = "map_comp";
 val map_comp'N = "map_comp'";
-val map_congN = "map_cong";
+val map_cong0N = "map_cong0";
 val map_wpullN = "map_wpull";
 val rel_eqN = "rel_eq";
 val rel_flipN = "rel_flip";
@@ -814,7 +814,7 @@
         fold_rev Logic.all (fs @ gs) (mk_Trueprop_eq (bnf_map_app_comp, comp_bnf_map_app))
       end;
 
-    val map_cong_goal =
+    val map_cong0_goal =
       let
         fun mk_prem z set f f_copy =
           Logic.all z (Logic.mk_implies
@@ -890,7 +890,7 @@
 
     val srel_O_Gr_goal = fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (srel, Rs), O_Gr));
 
-    val goals = zip_axioms map_id_goal map_comp_goal map_cong_goal set_naturals_goal
+    val goals = zip_axioms map_id_goal map_comp_goal map_cong0_goal set_naturals_goal
       card_order_bd_goal cinfinite_bd_goal set_bds_goal in_bd_goal map_wpull_goal srel_O_Gr_goal;
 
     fun mk_wit_goals (I, wit) =
@@ -1004,7 +1004,7 @@
                 (Logic.list_implies (prems, HOLogic.mk_Trueprop concl))
           in
             Goal.prove_sorry lthy [] [] goal
-              (fn _ => mk_map_wppull_tac (#map_id axioms) (#map_cong axioms)
+              (fn _ => mk_map_wppull_tac (#map_id axioms) (#map_cong0 axioms)
                 (#map_wpull axioms) (Lazy.force map_comp') (map Lazy.force set_natural'))
             |> Thm.close_derivation
           end;
@@ -1020,7 +1020,7 @@
             val goal = fold_rev Logic.all (As @ fs) (mk_Trueprop_eq (lhs, rhs));
           in
             Goal.prove_sorry lthy [] [] goal
-              (mk_srel_Gr_tac srel_O_Grs (#map_id axioms) (#map_cong axioms) (Lazy.force map_id')
+              (mk_srel_Gr_tac srel_O_Grs (#map_id axioms) (#map_cong0 axioms) (Lazy.force map_id')
                 (Lazy.force map_comp') (map Lazy.force set_natural'))
             |> Thm.close_derivation
           end;
@@ -1074,7 +1074,7 @@
             val rhs = mk_converse (Term.list_comb (srel, Rs));
             val le_goal = fold_rev Logic.all Rs (HOLogic.mk_Trueprop (mk_subset lhs rhs));
             val le_thm = Goal.prove_sorry lthy [] [] le_goal
-              (mk_srel_converse_le_tac srel_O_Grs (Lazy.force srel_Id) (#map_cong axioms)
+              (mk_srel_converse_le_tac srel_O_Grs (Lazy.force srel_Id) (#map_cong0 axioms)
                 (Lazy.force map_comp') (map Lazy.force set_natural'))
               |> Thm.close_derivation
             val goal = fold_rev Logic.all Rs (mk_Trueprop_eq (lhs, rhs));
@@ -1094,7 +1094,7 @@
             val goal = fold_rev Logic.all (Rs @ Ss) (mk_Trueprop_eq (lhs, rhs));
           in
             Goal.prove_sorry lthy [] [] goal
-              (mk_srel_O_tac srel_O_Grs (Lazy.force srel_Id) (#map_cong axioms)
+              (mk_srel_O_tac srel_O_Grs (Lazy.force srel_Id) (#map_cong0 axioms)
                 (Lazy.force map_wppull) (Lazy.force map_comp') (map Lazy.force set_natural'))
             |> Thm.close_derivation
           end;
@@ -1201,7 +1201,7 @@
                 let
                   val notes =
                     [(map_comp'N, [Lazy.force (#map_comp' facts)]),
-                    (map_congN, [#map_cong axioms]),
+                    (map_cong0N, [#map_cong0 axioms]),
                     (map_id'N, [Lazy.force (#map_id' facts)]),
                     (rel_eqN, [Lazy.force (#rel_eq facts)]),
                     (rel_flipN, [Lazy.force (#rel_flip facts)]),
diff -r e5ce85418346 -r 4c9f08836d87 src/HOL/BNF/Tools/bnf_def_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML	Wed Apr 24 14:14:36 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML	Wed Apr 24 14:15:01 2013 +0200
@@ -51,7 +51,7 @@
     rtac set_natural) set_naturals) THEN'
   rtac @{thm image_empty}) 1;
 
-fun mk_map_wppull_tac map_id map_cong map_wpull map_comp set_naturals =
+fun mk_map_wppull_tac map_id map_cong0 map_wpull map_comp set_naturals =
   if null set_naturals then
     EVERY' [rtac @{thm wppull_id}, rtac map_wpull, rtac map_id, rtac map_id] 1
   else EVERY' [REPEAT_DETERM o etac conjE, REPEAT_DETERM o dtac @{thm wppull_thePull},
@@ -62,12 +62,12 @@
       rtac @{thm image_subsetI}, rtac conjunct1, etac bspec, etac set_mp, atac])
       set_naturals,
     CONJ_WRAP' (fn thm => EVERY' [rtac (map_comp RS trans), rtac (map_comp RS trans),
-      rtac (map_comp RS trans RS sym), rtac map_cong,
+      rtac (map_comp RS trans RS sym), rtac map_cong0,
       REPEAT_DETERM_N (length set_naturals) 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_srel_Gr_tac srel_O_Grs map_id map_cong map_id' map_comp set_naturals
+fun mk_srel_Gr_tac srel_O_Grs map_id map_cong0 map_id' map_comp set_naturals
   {context = ctxt, prems = _} =
   let
     val n = length set_naturals;
@@ -80,7 +80,7 @@
         REPEAT_DETERM o dtac Pair_eqD,
         REPEAT_DETERM o etac conjE, hyp_subst_tac,
         rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
-        rtac sym, rtac trans, rtac map_comp, rtac map_cong,
+        rtac sym, rtac trans, rtac map_comp, rtac map_cong0,
         REPEAT_DETERM_N n o EVERY' [dtac @{thm set_rev_mp}, atac,
           REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
           rtac (o_apply RS trans), rtac (@{thm fst_conv} RS arg_cong RS trans),
@@ -97,7 +97,7 @@
         EVERY' (map2 (fn convol => fn map_id =>
           EVERY' [rtac CollectI, rtac exI, rtac conjI,
             rtac Pair_eqI, rtac conjI, rtac refl, rtac sym,
-            rtac (box_equals OF [map_cong, map_comp RS sym, map_id]),
+            rtac (box_equals OF [map_cong0, map_comp RS sym, map_id]),
             REPEAT_DETERM_N n o rtac (convol RS fun_cong),
             REPEAT_DETERM o eresolve_tac [CollectE, conjE],
             rtac CollectI,
@@ -121,7 +121,7 @@
       rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac,
       rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac] 1;
 
-fun mk_srel_converse_le_tac srel_O_Grs srel_Id map_cong map_comp set_naturals
+fun mk_srel_converse_le_tac srel_O_Grs srel_Id map_cong0 map_comp set_naturals
   {context = ctxt, prems = _} =
   let
     val n = length set_naturals;
@@ -136,7 +136,7 @@
         rtac @{thm relcompI}, rtac @{thm converseI},
         EVERY' (map (fn thm => EVERY' [rtac CollectI, rtac exI,
           rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, rtac trans,
-          rtac map_cong, REPEAT_DETERM_N n o rtac thm,
+          rtac map_cong0, REPEAT_DETERM_N n o rtac thm,
           rtac (map_comp RS sym), rtac CollectI,
           CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
             etac @{thm flip_rel}]) set_naturals]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1
@@ -146,7 +146,7 @@
   EVERY' [rtac equalityI, rtac le_converse, rtac @{thm xt1(6)}, rtac @{thm converse_shift},
     rtac le_converse, REPEAT_DETERM o stac @{thm converse_converse}, rtac subset_refl] 1;
 
-fun mk_srel_O_tac srel_O_Grs srel_Id map_cong map_wppull map_comp set_naturals
+fun mk_srel_O_tac srel_O_Grs srel_Id map_cong0 map_wppull map_comp set_naturals
   {context = ctxt, prems = _} =
   let
     val n = length set_naturals;
@@ -162,22 +162,22 @@
         REPEAT_DETERM o etac conjE, hyp_subst_tac,
         rtac @{thm relcompI}, rtac @{thm relcompI}, rtac @{thm converseI},
         rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
-        rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong,
+        rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong0,
         REPEAT_DETERM_N n o rtac @{thm fst_fstO},
         in_tac @{thm fstO_in},
         rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
-        rtac sym, rtac trans, rtac map_comp, rtac map_cong,
+        rtac sym, rtac trans, rtac map_comp, 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_fstO_sndO}, atac, etac notE,
           etac set_mp, atac],
         in_tac @{thm fstO_in},
         rtac @{thm relcompI}, rtac @{thm converseI},
         rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
-        rtac sym, rtac trans, rtac map_comp, rtac map_cong,
+        rtac sym, rtac trans, rtac map_comp, rtac map_cong0,
         REPEAT_DETERM_N n o rtac o_apply,
         in_tac @{thm sndO_in},
         rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
-        rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong,
+        rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong0,
         REPEAT_DETERM_N n o rtac @{thm snd_sndO},
         in_tac @{thm sndO_in},
         rtac @{thm subrelI},
@@ -192,7 +192,7 @@
         rtac @{thm relcompI}, rtac @{thm converseI},
         EVERY' (map (fn thm => EVERY' [rtac CollectI, rtac exI,
           rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, rtac sym, rtac trans,
-          rtac trans, rtac map_cong, REPEAT_DETERM_N n o rtac thm,
+          rtac trans, rtac map_cong0, REPEAT_DETERM_N n o rtac thm,
           rtac (map_comp RS sym), atac, atac]) [@{thm fst_fstO}, @{thm snd_sndO}])] 1
   end;
 
diff -r e5ce85418346 -r 4c9f08836d87 src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Wed Apr 24 14:14:36 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Wed Apr 24 14:15:01 2013 +0200
@@ -222,7 +222,7 @@
     val map_comps = map map_comp_of_bnf bnfs;
     val sym_map_comps = map (fn thm => thm RS sym) map_comps;
     val map_comp's = map map_comp'_of_bnf bnfs;
-    val map_congs = map map_cong_of_bnf bnfs;
+    val map_cong0s = map map_cong0_of_bnf bnfs;
     val map_ids = map map_id_of_bnf bnfs;
     val map_id's = map map_id'_of_bnf bnfs;
     val map_wpulls = map map_wpull_of_bnf bnfs;
@@ -260,7 +260,7 @@
 
     (*forall a : set(m+1) x. f(m+1) a = a; ...; forall a : set(m+n) x. f(m+n) a = a ==>
       map id ... id f(m+1) ... f(m+n) x = x*)
-    fun mk_map_congL x mapAsAs sets map_cong map_id' =
+    fun mk_map_cong0L x mapAsAs sets map_cong0 map_id' =
       let
         fun mk_prem set f z z' =
           HOLogic.mk_Trueprop
@@ -270,11 +270,11 @@
       in
         Goal.prove_sorry lthy [] []
           (fold_rev Logic.all (x :: self_fs) (Logic.list_implies (prems, goal)))
-          (K (mk_map_congL_tac m map_cong map_id'))
+          (K (mk_map_cong0L_tac m map_cong0 map_id'))
         |> Thm.close_derivation
       end;
 
-    val map_congL_thms = map5 mk_map_congL xFs mapsAsAs setssAs map_congs map_id's;
+    val map_cong0L_thms = map5 mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_id's;
     val in_mono'_thms = map (fn thm =>
       (thm OF (replicate m subset_refl)) RS @{thm set_mp}) in_monos;
 
@@ -866,7 +866,7 @@
         Goal.prove_sorry lthy [] []
           (fold_rev Logic.all (As @ Bs @ ss @ B's @ s's @ Rs)
             (mk_Trueprop_eq (mk_bis As Bs ss B's s's Rs, rhs)))
-          (K (mk_bis_srel_tac m bis_def srel_O_Grs map_comp's map_congs set_natural'ss))
+          (K (mk_bis_srel_tac m bis_def srel_O_Grs map_comp's map_cong0s set_natural'ss))
         |> Thm.close_derivation
       end;
 
@@ -1770,7 +1770,7 @@
           to_sbd_inj_thmss from_to_sbd_thmss Lev_0s Lev_Sucs rv_Nils rv_Conss Lev_sbd_thms
           length_Lev_thms length_Lev'_thms prefCl_Lev_thms rv_last_thmss
           set_rv_Lev_thmsss set_Lev_thmsss set_image_Lev_thmsss
-          set_natural'ss coalg_set_thmss map_comp_id_thms map_congs map_arg_cong_thms)
+          set_natural'ss coalg_set_thmss map_comp_id_thms map_cong0s map_arg_cong_thms)
       |> Thm.close_derivation;
 
     val timer = time (timer "Behavioral morphism");
@@ -1799,11 +1799,11 @@
 
         val goals = map3 mk_goal (map (mk_LSBIS As) ks) final_maps strTAs;
       in
-        map4 (fn goal => fn lsbisE => fn map_comp_id => fn map_cong =>
+        map4 (fn goal => fn lsbisE => fn map_comp_id => fn map_cong0 =>
           Goal.prove_sorry lthy [] [] goal
-            (K (mk_congruent_str_final_tac m lsbisE map_comp_id map_cong equiv_LSBIS_thms))
+            (K (mk_congruent_str_final_tac m lsbisE map_comp_id map_cong0 equiv_LSBIS_thms))
           |> Thm.close_derivation)
-        goals lsbisE_thms map_comp_id_thms map_congs
+        goals lsbisE_thms map_comp_id_thms map_cong0s
       end;
 
     val coalg_final_thm = Goal.prove_sorry lthy [] [] (fold_rev Logic.all As
@@ -1919,7 +1919,7 @@
           Goal.prove_sorry lthy [] []
             (HOLogic.mk_Trueprop (mk_mor UNIVs dtors car_finals str_finals Rep_Ts))
             (mk_mor_Rep_tac m (mor_def :: dtor_defs) Reps Abs_inverses coalg_final_set_thmss
-              map_comp_id_thms map_congL_thms)
+              map_comp_id_thms map_cong0L_thms)
           |> Thm.close_derivation;
 
         val mor_Abs =
@@ -1974,7 +1974,7 @@
           (fold_rev Logic.all ss
             (HOLogic.mk_Trueprop (mk_mor active_UNIVs ss UNIVs dtors (map (mk_unfold Ts ss) ks))))
           (K (mk_mor_unfold_tac m mor_UNIV_thm dtor_defs unfold_defs Abs_inverses' morEs'
-            map_comp_id_thms map_congs))
+            map_comp_id_thms map_cong0s))
         |> Thm.close_derivation
       end;
     val dtor_unfold_thms = map (fn thm => (thm OF [mor_unfold_thm, UNIV_I]) RS sym) morE_thms;
@@ -2084,11 +2084,11 @@
          mk_Trueprop_eq (HOLogic.mk_comp (dtor, ctor), HOLogic.id_const FT);
         val goals = map3 mk_goal dtors ctors FTs;
       in
-        map5 (fn goal => fn ctor_def => fn unfold => fn map_comp_id => fn map_congL =>
+        map5 (fn goal => fn ctor_def => fn unfold => fn map_comp_id => fn map_cong0L =>
           Goal.prove_sorry lthy [] [] goal
-            (mk_dtor_o_ctor_tac ctor_def unfold map_comp_id map_congL unfold_o_dtor_thms)
+            (mk_dtor_o_ctor_tac ctor_def unfold map_comp_id map_cong0L unfold_o_dtor_thms)
           |> Thm.close_derivation)
-          goals ctor_defs dtor_unfold_thms map_comp_id_thms map_congL_thms
+          goals ctor_defs dtor_unfold_thms map_comp_id_thms map_cong0L_thms
       end;
 
     val dtor_ctor_thms = map (fn thm => thm RS @{thm pointfree_idE}) dtor_o_ctor_thms;
@@ -2175,11 +2175,11 @@
           end;
         val goals = map5 mk_goal ks corec_ss corec_maps_rev dtors zs;
       in
-        map3 (fn goal => fn unfold => fn map_cong =>
+        map3 (fn goal => fn unfold => fn map_cong0 =>
           Goal.prove_sorry lthy [] [] goal
-            (mk_corec_tac m corec_defs unfold map_cong corec_Inl_sum_thms)
+            (mk_corec_tac m corec_defs unfold map_cong0 corec_Inl_sum_thms)
           |> Thm.close_derivation)
-        goals dtor_unfold_thms map_congs
+        goals dtor_unfold_thms map_cong0s
       end;
 
     val corec_unique_mor_thm =
@@ -2409,11 +2409,11 @@
             val goals = map4 mk_goal fs_maps map_FTFT's dtors dtor's;
             val cTs = map (SOME o certifyT lthy) FTs';
             val maps =
-              map5 (fn goal => fn cT => fn unfold => fn map_comp' => fn map_cong =>
+              map5 (fn goal => fn cT => fn unfold => fn map_comp' => fn map_cong0 =>
                 Goal.prove_sorry lthy [] [] goal
-                  (K (mk_map_tac m n cT unfold map_comp' map_cong))
+                  (K (mk_map_tac m n cT unfold map_comp' map_cong0))
                 |> Thm.close_derivation)
-              goals cTs dtor_unfold_thms map_comp's map_congs;
+              goals cTs dtor_unfold_thms map_comp's map_cong0s;
           in
             map_split (fn thm => (thm RS @{thm pointfreeE}, thm)) maps
           end;
@@ -2427,7 +2427,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_congs dtor_unfold_unique_thm))
+              (K (mk_map_comp_tac m n map_thms map_comps map_cong0s dtor_unfold_unique_thm))
               |> Thm.close_derivation)
           end;
 
@@ -2548,7 +2548,7 @@
             map (split_conj_thm o mk_specN n) thms
           end;
 
-        val map_cong_thms =
+        val map_cong0_thms =
           let
             val cTs = map (SOME o certifyT lthy o
               Term.typ_subst_atomic (passiveAs ~~ passiveBs) o TFree) coinduct_params;
@@ -2559,7 +2559,7 @@
             fun mk_prems sets z =
               Library.foldr1 HOLogic.mk_conj (map5 (mk_prem z) sets fs fs_copy ys ys')
 
-            fun mk_map_cong sets z fmap gmap =
+            fun mk_map_cong0 sets z fmap gmap =
               HOLogic.mk_imp (mk_prems sets z, HOLogic.mk_eq (fmap $ z, gmap $ z));
 
             fun mk_coind_body sets (x, T) z fmap gmap y y_copy =
@@ -2581,11 +2581,11 @@
 
             val goal =
               HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
-                (map4 mk_map_cong setss_by_bnf Jzs fs_maps fs_copy_maps));
+                (map4 mk_map_cong0 setss_by_bnf Jzs fs_maps fs_copy_maps));
 
             val thm = singleton (Proof_Context.export names_lthy lthy)
               (Goal.prove_sorry lthy [] [] goal
-              (K (mk_mcong_tac m (rtac coinduct) map_comp's dtor_map_thms map_congs set_natural'ss
+              (K (mk_mcong_tac m (rtac coinduct) map_comp's dtor_map_thms map_cong0s set_natural'ss
               set_hset_thmss set_hset_hset_thmsss)))
               |> Thm.close_derivation
           in
@@ -2685,7 +2685,7 @@
         val map_id_tacs =
           map2 (K oo mk_map_id_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_cong_tacs = map (mk_map_cong_tac m) map_cong_thms;
+        val map_cong0_tacs = map (mk_map_cong0_tac m) map_cong0_thms;
         val set_nat_tacss =
           map2 (map2 (K oo mk_set_natural_tac)) hset_defss (transpose col_natural_thmss);
 
@@ -2709,7 +2709,7 @@
 
         val srel_O_Gr_tacs = replicate n (simple_srel_O_Gr_tac o #context);
 
-        val tacss = map10 zip_axioms map_id_tacs map_comp_tacs map_cong_tacs set_nat_tacss
+        val tacss = map10 zip_axioms map_id_tacs map_comp_tacs map_cong0_tacs set_nat_tacss
           bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs srel_O_Gr_tacs;
 
         val (hset_dtor_incl_thmss, hset_hset_dtor_incl_thmsss, dtor_hset_induct_thms) =
@@ -2941,14 +2941,14 @@
                   HOLogic.mk_mem (HOLogic.mk_prod (dtor $ Jz, dtor' $ Jz'), srelR)));
             val goals = map6 mk_goal Jzs Jz's dtors dtor's JsrelRs srelRs;
           in
-            map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong =>
+            map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong0 =>
               fn dtor_map => fn dtor_sets => fn dtor_inject => fn dtor_ctor =>
               fn set_naturals => fn dtor_set_incls => fn dtor_set_set_inclss =>
               Goal.prove_sorry lthy [] [] goal
-                (K (mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong dtor_map dtor_sets
+                (K (mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong0 dtor_map dtor_sets
                   dtor_inject dtor_ctor set_naturals dtor_set_incls dtor_set_set_inclss))
               |> Thm.close_derivation)
-            ks goals in_srels map_comp's map_congs folded_dtor_map_thms folded_dtor_set_thmss'
+            ks goals in_srels map_comp's map_cong0s folded_dtor_map_thms folded_dtor_set_thmss'
               dtor_inject_thms dtor_ctor_thms set_natural'ss dtor_set_incl_thmss
               dtor_set_set_incl_thmsss
           end;
diff -r e5ce85418346 -r 4c9f08836d87 src/HOL/BNF/Tools/bnf_gfp_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Wed Apr 24 14:14:36 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Wed Apr 24 14:15:01 2013 +0200
@@ -256,12 +256,12 @@
   EVERY' [rtac (hset_def RS trans), rtac (refl RS @{thm UN_cong} RS trans), etac mor_hset_rec,
     atac, atac, rtac (hset_def RS sym)] 1
 
-fun mk_bis_srel_tac m bis_def srel_O_Grs map_comps map_congs set_naturalss =
+fun mk_bis_srel_tac m bis_def srel_O_Grs map_comps map_cong0s set_naturalss =
   let
     val n = length srel_O_Grs;
-    val thms = ((1 upto n) ~~ map_comps ~~ map_congs ~~ set_naturalss ~~ srel_O_Grs);
+    val thms = ((1 upto n) ~~ map_comps ~~ map_cong0s ~~ set_naturalss ~~ srel_O_Grs);
 
-    fun mk_if_tac ((((i, map_comp), map_cong), set_naturals), srel_O_Gr) =
+    fun mk_if_tac ((((i, map_comp), map_cong0), set_naturals), srel_O_Gr) =
       EVERY' [rtac allI, rtac allI, rtac impI, dtac (mk_conjunctN n i),
         etac allE, etac allE, etac impE, atac, etac bexE, etac conjE,
         rtac (srel_O_Gr RS equalityD2 RS set_mp),
@@ -276,11 +276,11 @@
               else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm,
                 rtac trans_fun_cong_image_id_id_apply, atac])
             (1 upto (m + n) ~~ set_naturals),
-            rtac trans, rtac trans, rtac map_comp, rtac map_cong, REPEAT_DETERM_N m o rtac thm,
+            rtac trans, rtac trans, rtac map_comp, rtac map_cong0, REPEAT_DETERM_N m o rtac thm,
             REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), atac])
           @{thms fst_diag_id snd_diag_id})];
 
-    fun mk_only_if_tac ((((i, map_comp), map_cong), set_naturals), srel_O_Gr) =
+    fun mk_only_if_tac ((((i, map_comp), map_cong0), set_naturals), srel_O_Gr) =
       EVERY' [dtac (mk_conjunctN n i), rtac allI, rtac allI, rtac impI,
         etac allE, etac allE, etac impE, atac,
         dtac (srel_O_Gr RS equalityD1 RS set_mp),
@@ -290,13 +290,13 @@
         REPEAT_DETERM o etac conjE,
         hyp_subst_tac,
         REPEAT_DETERM o eresolve_tac [CollectE, conjE],
-        rtac bexI, rtac conjI, rtac trans, rtac map_comp, rtac trans, rtac map_cong,
+        rtac bexI, rtac conjI, rtac trans, rtac map_comp, 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),
-        etac sym, rtac trans, rtac map_comp, rtac trans, rtac map_cong,
+        etac sym, rtac trans, rtac map_comp, 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_cong,
+        rtac trans, rtac map_cong0,
         REPEAT_DETERM_N m o EVERY' [rtac @{thm Id_onD'}, etac set_mp, atac],
         REPEAT_DETERM_N n o rtac refl,
         etac sym, rtac CollectI,
@@ -841,7 +841,7 @@
 fun mk_mor_beh_tac m mor_def mor_cong beh_defs carT_defs strT_defs isNode_defs
   to_sbd_injss from_to_sbdss Lev_0s Lev_Sucs rv_Nils rv_Conss Lev_sbds length_Levs length_Lev's
   prefCl_Levs rv_lastss set_rv_Levsss set_Levsss set_image_Levsss set_naturalss coalg_setss
-  map_comp_ids map_congs map_arg_congs {context = ctxt, prems = _} =
+  map_comp_ids map_cong0s map_arg_congs {context = ctxt, prems = _} =
   let
     val n = length beh_defs;
     val ks = 1 upto n;
@@ -939,7 +939,7 @@
           (drop m set_naturals ~~ (nth set_Levss (i - 1) ~~ nth set_image_Levss (i - 1)))];
 
     fun mor_tac (i, (strT_def, (((Lev_0, Lev_Suc), (rv_Nil, rv_Cons)),
-      ((map_comp_id, (map_cong, map_arg_cong)), (length_Lev', (from_to_sbds, to_sbd_injs)))))) =
+      ((map_comp_id, (map_cong0, map_arg_cong)), (length_Lev', (from_to_sbds, to_sbd_injs)))))) =
       EVERY' [rtac ballI, rtac sym, rtac trans, rtac strT_def,
         rtac (@{thm if_P} RS
           (if n = 1 then map_arg_cong else sum_case_weak_cong) RS trans),
@@ -950,7 +950,7 @@
         if n = 1 then K all_tac
         else (rtac (sum_case_weak_cong RS trans) THEN'
           rtac (mk_sum_casesN n i) THEN' rtac (mk_sum_casesN n i RS trans)),
-        rtac (map_comp_id RS trans), rtac (map_cong OF replicate m refl),
+        rtac (map_comp_id RS trans), rtac (map_cong0 OF replicate m refl),
         EVERY' (map3 (fn i' => fn to_sbd_inj => fn from_to_sbd =>
           DETERM o EVERY' [rtac trans, rtac o_apply, rtac Pair_eqI, rtac conjI,
             rtac trans, rtac @{thm Shift_def},
@@ -1001,15 +1001,15 @@
             (set_rv_Levsss ~~ (set_Levsss ~~ set_image_Levsss))))))))))))) THEN'
     CONJ_WRAP' mor_tac
       (ks ~~ (strT_defs ~~ (((Lev_0s ~~ Lev_Sucs) ~~ (rv_Nils ~~ rv_Conss)) ~~
-        ((map_comp_ids ~~ (map_congs ~~ map_arg_congs)) ~~
+        ((map_comp_ids ~~ (map_cong0s ~~ map_arg_congs)) ~~
           (length_Lev's ~~ (from_to_sbdss ~~ to_sbd_injss))))))) 1
   end;
 
-fun mk_congruent_str_final_tac m lsbisE map_comp_id map_cong equiv_LSBISs =
+fun mk_congruent_str_final_tac m lsbisE map_comp_id map_cong0 equiv_LSBISs =
   EVERY' [rtac @{thm congruentI}, dtac lsbisE,
     REPEAT_DETERM o eresolve_tac [CollectE, conjE, bexE], rtac (o_apply RS trans),
     etac (sym RS arg_cong RS trans), rtac (map_comp_id RS trans),
-    rtac (map_cong RS trans), REPEAT_DETERM_N m o rtac refl,
+    rtac (map_cong0 RS trans), REPEAT_DETERM_N m o rtac refl,
     EVERY' (map (fn equiv_LSBIS =>
       EVERY' [rtac @{thm equiv_proj}, rtac equiv_LSBIS, etac set_mp, atac])
     equiv_LSBISs), rtac sym, rtac (o_apply RS trans),
@@ -1042,18 +1042,18 @@
         rtac congruent_str_final, atac, rtac o_apply])
     (equiv_LSBISs ~~ congruent_str_finals)] 1;
 
-fun mk_mor_Rep_tac m defs Reps Abs_inverses coalg_final_setss map_comp_ids map_congLs
+fun mk_mor_Rep_tac m defs Reps Abs_inverses coalg_final_setss map_comp_ids map_cong0Ls
   {context = ctxt, prems = _} =
   unfold_thms_tac ctxt defs THEN
   EVERY' [rtac conjI,
     CONJ_WRAP' (fn thm => rtac ballI THEN' rtac thm) Reps,
-    CONJ_WRAP' (fn (Rep, ((map_comp_id, map_congL), coalg_final_sets)) =>
-      EVERY' [rtac ballI, rtac (map_comp_id RS trans), rtac map_congL,
+    CONJ_WRAP' (fn (Rep, ((map_comp_id, map_cong0L), coalg_final_sets)) =>
+      EVERY' [rtac ballI, rtac (map_comp_id RS trans), rtac map_cong0L,
         EVERY' (map2 (fn Abs_inverse => fn coalg_final_set =>
           EVERY' [rtac ballI, rtac (o_apply RS trans), rtac Abs_inverse,
             etac set_rev_mp, rtac coalg_final_set, rtac Rep])
         Abs_inverses (drop m coalg_final_sets))])
-    (Reps ~~ ((map_comp_ids ~~ map_congLs) ~~ coalg_final_setss))] 1;
+    (Reps ~~ ((map_comp_ids ~~ map_cong0Ls) ~~ coalg_final_setss))] 1;
 
 fun mk_mor_Abs_tac defs Abs_inverses {context = ctxt, prems = _} =
   unfold_thms_tac ctxt defs THEN
@@ -1061,16 +1061,16 @@
     CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) Abs_inverses,
     CONJ_WRAP' (fn thm => rtac ballI THEN' etac (thm RS arg_cong RS sym)) Abs_inverses] 1;
 
-fun mk_mor_unfold_tac m mor_UNIV dtor_defs unfold_defs Abs_inverses morEs map_comp_ids map_congs =
+fun mk_mor_unfold_tac m mor_UNIV dtor_defs unfold_defs Abs_inverses morEs map_comp_ids map_cong0s =
   EVERY' [rtac iffD2, rtac mor_UNIV,
-    CONJ_WRAP' (fn ((Abs_inverse, morE), ((dtor_def, unfold_def), (map_comp_id, map_cong))) =>
+    CONJ_WRAP' (fn ((Abs_inverse, morE), ((dtor_def, unfold_def), (map_comp_id, map_cong0))) =>
       EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (dtor_def RS trans),
         rtac (unfold_def RS arg_cong RS trans), rtac (Abs_inverse RS arg_cong RS trans),
         rtac (morE RS arg_cong RS trans), rtac (map_comp_id RS trans),
-        rtac (o_apply RS trans RS sym), rtac map_cong,
+        rtac (o_apply RS trans RS sym), rtac map_cong0,
         REPEAT_DETERM_N m o rtac refl,
         EVERY' (map (fn thm => rtac (thm RS trans) THEN' rtac (o_apply RS sym)) unfold_defs)])
-    ((Abs_inverses ~~ morEs) ~~ ((dtor_defs ~~ unfold_defs) ~~ (map_comp_ids ~~ map_congs)))] 1;
+    ((Abs_inverses ~~ morEs) ~~ ((dtor_defs ~~ unfold_defs) ~~ (map_comp_ids ~~ map_cong0s)))] 1;
 
 fun mk_raw_coind_tac bis_def bis_cong bis_O bis_converse bis_Gr tcoalg coalgT mor_T_final
   sbis_lsbis lsbis_incls incl_lsbiss equiv_LSBISs mor_Rep Rep_injects =
@@ -1109,17 +1109,17 @@
       rtac @{thm image2_eqI}, rtac refl, rtac (unfold_def RS arg_cong RS trans),
       rtac (o_apply RS sym), rtac UNIV_I]) (raw_coinds ~~ unfold_defs) 1;
 
-fun mk_dtor_o_ctor_tac ctor_def unfold map_comp_id map_congL unfold_o_dtors
+fun mk_dtor_o_ctor_tac ctor_def unfold map_comp_id map_cong0L unfold_o_dtors
   {context = ctxt, prems = _} =
   unfold_thms_tac ctxt [ctor_def] THEN EVERY' [rtac ext, rtac trans, rtac o_apply,
-    rtac trans, rtac unfold, rtac trans, rtac map_comp_id, rtac trans, rtac map_congL,
+    rtac trans, rtac unfold, rtac trans, rtac map_comp_id, rtac trans, rtac map_cong0L,
     EVERY' (map (fn thm =>
       rtac ballI THEN' rtac (trans OF [thm RS fun_cong, id_apply])) unfold_o_dtors),
     rtac sym, rtac id_apply] 1;
 
-fun mk_corec_tac m corec_defs unfold map_cong corec_Inls {context = ctxt, prems = _} =
+fun mk_corec_tac m corec_defs unfold map_cong0 corec_Inls {context = ctxt, prems = _} =
   unfold_thms_tac ctxt corec_defs THEN EVERY' [rtac trans, rtac (o_apply RS arg_cong),
-    rtac trans, rtac unfold, fo_rtac (@{thm sum.cases(2)} RS arg_cong RS trans) ctxt, rtac map_cong,
+    rtac trans, rtac unfold, fo_rtac (@{thm sum.cases(2)} RS arg_cong RS trans) ctxt, rtac map_cong0,
     REPEAT_DETERM_N m o rtac refl,
     EVERY' (map (fn thm => rtac @{thm sum_case_expand_Inr} THEN' rtac thm) corec_Inls)] 1;
 
@@ -1184,9 +1184,9 @@
     rtac impI, REPEAT_DETERM o etac conjE,
     CONJ_WRAP' (K (rtac impI THEN' etac mp THEN' etac disjI1)) ks] 1;
 
-fun mk_map_tac m n cT unfold map_comp' map_cong =
+fun mk_map_tac m n cT unfold map_comp' map_cong0 =
   EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (o_apply RS trans RS sym),
-    rtac (unfold RS trans), rtac (Thm.permute_prems 0 1 (map_comp' RS box_equals)), rtac map_cong,
+    rtac (unfold RS trans), rtac (Thm.permute_prems 0 1 (map_comp' RS box_equals)), 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 (o_apply RS (Drule.instantiate' [cT] [] arg_cong) RS sym)] 1;
@@ -1210,9 +1210,9 @@
   EVERY' [rtac (unfold_unique RS trans), EVERY' (map (fn thm => rtac (thm RS sym)) maps),
     rtac unfold_dtor] 1;
 
-fun mk_map_comp_tac m n maps map_comps map_congs unfold_unique =
+fun mk_map_comp_tac m n maps map_comps map_cong0s unfold_unique =
   EVERY' [rtac unfold_unique,
-    EVERY' (map3 (fn map_thm => fn map_comp => fn map_cong =>
+    EVERY' (map3 (fn map_thm => fn map_comp => 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,
@@ -1220,12 +1220,12 @@
         @{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,
-        ext, o_apply RS trans,  o_apply RS trans RS sym, map_cong] @
+        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_congs)] 1;
+    maps map_comps map_cong0s)] 1;
 
-fun mk_mcong_tac m coinduct_tac map_comp's dtor_maps map_congs set_naturalss set_hsetss
+fun mk_mcong_tac m coinduct_tac map_comp's dtor_maps map_cong0s set_naturalss set_hsetss
   set_hset_hsetsss =
   let
     val n = length map_comp's;
@@ -1233,13 +1233,13 @@
   in
     EVERY' ([rtac rev_mp,
       coinduct_tac] @
-      maps (fn (((((map_comp'_trans, dtor_maps_trans), map_cong), set_naturals), set_hsets),
+      maps (fn (((((map_comp'_trans, dtor_maps_trans), map_cong0), set_naturals), set_hsets),
         set_hset_hsetss) =>
         [REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI, rtac conjI, rtac conjI,
-         rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong,
+         rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong0,
          REPEAT_DETERM_N m o (rtac o_apply_trans_sym THEN' rtac id_apply),
          REPEAT_DETERM_N n o rtac fst_convol_fun_cong_sym,
-         rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong,
+         rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong0,
          EVERY' (maps (fn set_hset =>
            [rtac o_apply_trans_sym, rtac (id_apply RS trans), etac CollectE,
            REPEAT_DETERM o etac conjE, etac bspec, etac set_hset]) set_hsets),
@@ -1253,7 +1253,7 @@
                EVERY' [rtac ballI, etac bspec, etac set_hset_hset, atac]) set_hset_hsets])
            (drop m set_naturals ~~ set_hset_hsetss)])
         (map (fn th => th RS trans) map_comp's ~~ map (fn th => th RS trans) dtor_maps ~~
-          map_congs ~~ set_naturalss ~~ set_hsetss ~~ set_hset_hsetsss) @
+          map_cong0s ~~ set_naturalss ~~ set_hsetss ~~ set_hset_hsetsss) @
       [rtac impI,
        CONJ_WRAP' (fn k =>
          EVERY' [rtac impI, dtac (mk_conjunctN n k), etac mp, rtac exI, rtac conjI, etac CollectI,
@@ -1499,7 +1499,7 @@
   ALLGOALS (TRY o
     FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE])
 
-fun mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong dtor_map dtor_sets dtor_inject dtor_ctor
+fun mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong0 dtor_map dtor_sets dtor_inject dtor_ctor
   set_naturals dtor_set_incls dtor_set_set_inclss =
   let
     val m = length dtor_set_incls;
@@ -1521,7 +1521,7 @@
             rtac conjI, rtac refl, rtac refl])
         (in_Jsrels ~~ (active_set_naturals ~~ dtor_set_set_inclss)),
         CONJ_WRAP' (fn conv =>
-          EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong,
+          EVERY' [rtac trans, rtac map_comp, 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])
@@ -1547,7 +1547,7 @@
         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 map_cong, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
+          rtac map_cong0, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
           EVERY' (map (fn in_Jsrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
             dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Jsrel RS iffD1),
             dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE, atac]) in_Jsrels),
diff -r e5ce85418346 -r 4c9f08836d87 src/HOL/BNF/Tools/bnf_lfp.ML
--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Wed Apr 24 14:14:36 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Wed Apr 24 14:15:01 2013 +0200
@@ -144,7 +144,7 @@
     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 map_comp's = map map_comp'_of_bnf bnfs;
-    val map_congs = map map_cong_of_bnf bnfs;
+    val map_cong0s = map map_cong0_of_bnf bnfs;
     val map_ids = map map_id_of_bnf bnfs;
     val map_id's = map map_id'_of_bnf bnfs;
     val map_wpulls = map map_wpull_of_bnf bnfs;
@@ -195,7 +195,7 @@
 
     (*forall a : set(m+1) x. f(m+1) a = a; ...; forall a : set(m+n) x. f(m+n) a = a ==>
       map id ... id f(m+1) ... f(m+n) x = x*)
-    fun mk_map_congL x mapAsAs sets map_cong map_id' =
+    fun mk_map_cong0L x mapAsAs sets map_cong0 map_id' =
       let
         fun mk_prem set f z z' = HOLogic.mk_Trueprop
           (mk_Ball (set $ x) (Term.absfree z' (HOLogic.mk_eq (f $ z, z))));
@@ -204,11 +204,11 @@
       in
         Goal.prove_sorry lthy [] []
           (fold_rev Logic.all (x :: self_fs) (Logic.list_implies (prems, goal)))
-          (K (mk_map_congL_tac m map_cong map_id'))
+          (K (mk_map_cong0L_tac m map_cong0 map_id'))
         |> Thm.close_derivation
       end;
 
-    val map_congL_thms = map5 mk_map_congL xFs mapsAsAs setssAs map_congs map_id's;
+    val map_cong0L_thms = map5 mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_id's;
     val in_mono'_thms = map (fn bnf => in_mono_of_bnf bnf OF (replicate m subset_refl)) bnfs;
     val in_cong'_thms = map (fn bnf => in_cong_of_bnf bnf OF (replicate m refl)) bnfs;
 
@@ -407,7 +407,7 @@
           (fold_rev Logic.all (Bs @ ss @ B's @ s's @ fs @ inv_fs)
             (Logic.list_implies (prems, concl)))
           (K (mk_mor_inv_tac alg_def mor_def
-            set_natural'ss morE_thms map_comp_id_thms map_congL_thms))
+            set_natural'ss morE_thms map_comp_id_thms map_cong0L_thms))
         |> Thm.close_derivation
       end;
 
@@ -897,7 +897,7 @@
           (fold_rev Logic.all (init_xs @ Bs @ ss @ init_fs @ init_fs_copy)
             (Logic.list_implies (prems @ mor_prems, unique)))
           (K (mk_init_unique_mor_tac m alg_def alg_init_thm least_min_alg_thms
-            in_mono'_thms alg_set_thms morE_thms map_congs))
+            in_mono'_thms alg_set_thms morE_thms map_cong0s))
           |> Thm.close_derivation;
       in
         (ex_mor, split_conj_thm unique_mor)
@@ -1180,11 +1180,11 @@
           mk_Trueprop_eq (HOLogic.mk_comp (dtor, ctor), HOLogic.id_const FT);
         val goals = map3 mk_goal dtors ctors FTs;
       in
-        map5 (fn goal => fn dtor_def => fn foldx => fn map_comp_id => fn map_congL =>
+        map5 (fn goal => fn dtor_def => fn foldx => fn map_comp_id => fn map_cong0L =>
           Goal.prove_sorry lthy [] [] goal
-            (K (mk_dtor_o_ctor_tac dtor_def foldx map_comp_id map_congL ctor_o_fold_thms))
+            (K (mk_dtor_o_ctor_tac dtor_def foldx map_comp_id map_cong0L ctor_o_fold_thms))
           |> Thm.close_derivation)
-        goals dtor_defs ctor_fold_thms map_comp_id_thms map_congL_thms
+        goals dtor_defs ctor_fold_thms map_comp_id_thms map_cong0L_thms
       end;
 
     val dtor_ctor_thms = map (fn thm => thm RS @{thm pointfree_idE}) dtor_o_ctor_thms;
@@ -1431,10 +1431,10 @@
                 HOLogic.mk_comp (ctor', Term.list_comb (map, fs @ fs_maps))));
             val goals = map4 mk_goal fs_maps map_FTFT's ctors ctor's;
             val maps =
-              map4 (fn goal => fn foldx => fn map_comp_id => fn map_cong =>
-                Goal.prove_sorry lthy [] [] goal (K (mk_map_tac m n foldx map_comp_id map_cong))
+              map4 (fn goal => fn foldx => fn map_comp_id => fn map_cong0 =>
+                Goal.prove_sorry lthy [] [] goal (K (mk_map_tac m n foldx map_comp_id map_cong0))
                 |> Thm.close_derivation)
-              goals ctor_fold_thms map_comp_id_thms map_congs;
+              goals ctor_fold_thms map_comp_id_thms map_cong0s;
           in
             map (fn thm => thm RS @{thm pointfreeE}) maps
           end;
@@ -1450,7 +1450,7 @@
                 (map2 (curry HOLogic.mk_eq) us fs_maps));
             val unique = Goal.prove_sorry lthy [] []
               (fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal)))
-              (K (mk_ctor_map_unique_tac m mor_def fold_unique_mor_thm map_comp_id_thms map_congs))
+              (K (mk_ctor_map_unique_tac m mor_def fold_unique_mor_thm map_comp_id_thms map_cong0s))
               |> Thm.close_derivation;
           in
             `split_conj_thm unique
@@ -1588,18 +1588,18 @@
             map split_conj_thm thms
           end;
 
-        val map_cong_thms =
+        val map_cong0_thms =
           let
             fun mk_prem z set f g y y' =
               mk_Ball (set $ z) (Term.absfree y' (HOLogic.mk_eq (f $ y, g $ y)));
 
-            fun mk_map_cong sets z fmap gmap =
+            fun mk_map_cong0 sets z fmap gmap =
               HOLogic.mk_imp
                 (Library.foldr1 HOLogic.mk_conj (map5 (mk_prem z) sets fs fs_copy ys ys'),
                 HOLogic.mk_eq (fmap $ z, gmap $ z));
 
             fun mk_cphi sets z fmap gmap =
-              certify lthy (Term.absfree (dest_Free z) (mk_map_cong sets z fmap gmap));
+              certify lthy (Term.absfree (dest_Free z) (mk_map_cong0 sets z fmap gmap));
 
             val cphis = map4 mk_cphi setss_by_bnf Izs fs_maps fs_copy_maps;
 
@@ -1607,11 +1607,11 @@
 
             val goal =
               HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
-                (map4 mk_map_cong setss_by_bnf Izs fs_maps fs_copy_maps));
+                (map4 mk_map_cong0 setss_by_bnf Izs fs_maps fs_copy_maps));
 
             val thm = singleton (Proof_Context.export names_lthy lthy)
               (Goal.prove_sorry lthy [] [] goal
-              (mk_mcong_tac (rtac induct) Fset_set_thmsss map_congs ctor_map_thms))
+              (mk_mcong_tac (rtac induct) Fset_set_thmsss map_cong0s ctor_map_thms))
               |> Thm.close_derivation;
           in
             split_conj_thm thm
@@ -1692,7 +1692,7 @@
         val map_id_tacs = map (K o mk_map_id_tac map_ids) 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_cong_tacs = map (mk_map_cong_tac m) map_cong_thms;
+        val map_cong0_tacs = map (mk_map_cong0_tac m) map_cong0_thms;
         val set_nat_tacss = map (map (K o mk_set_natural_tac)) (transpose set_natural_thmss);
         val bd_co_tacs = replicate n (K (mk_bd_card_order_tac bd_card_orders));
         val bd_cinf_tacs = replicate n (K (rtac (bd_Cinfinite RS conjunct1) 1));
@@ -1703,7 +1703,7 @@
 
         val srel_O_Gr_tacs = replicate n (simple_srel_O_Gr_tac o #context);
 
-        val tacss = map10 zip_axioms map_id_tacs map_comp_tacs map_cong_tacs set_nat_tacss
+        val tacss = map10 zip_axioms map_id_tacs map_comp_tacs map_cong0_tacs set_nat_tacss
           bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs srel_O_Gr_tacs;
 
         val ctor_witss =
@@ -1778,14 +1778,14 @@
                   HOLogic.mk_mem (HOLogic.mk_prod (xF, yF), srelR)));
             val goals = map6 mk_goal xFs yFs ctors ctor's IsrelRs srelRs;
           in
-            map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong =>
+            map12 (fn i => fn goal => fn in_srel => fn map_comp => fn map_cong0 =>
               fn ctor_map => fn ctor_sets => fn ctor_inject => fn ctor_dtor =>
               fn set_naturals => fn ctor_set_incls => fn ctor_set_set_inclss =>
               Goal.prove_sorry lthy [] [] goal
-               (K (mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong ctor_map ctor_sets
+               (K (mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong0 ctor_map ctor_sets
                  ctor_inject ctor_dtor set_naturals ctor_set_incls ctor_set_set_inclss))
               |> Thm.close_derivation)
-            ks goals in_srels map_comp's map_congs folded_ctor_map_thms folded_ctor_set_thmss'
+            ks goals in_srels map_comp's map_cong0s folded_ctor_map_thms folded_ctor_set_thmss'
               ctor_inject_thms ctor_dtor_thms set_natural'ss ctor_set_incl_thmss
               ctor_set_set_incl_thmsss
           end;
diff -r e5ce85418346 -r 4c9f08836d87 src/HOL/BNF/Tools/bnf_lfp_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Wed Apr 24 14:14:36 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Wed Apr 24 14:15:01 2013 +0200
@@ -139,7 +139,7 @@
     CONJ_WRAP' mor_tac (set_natural's ~~ map_comp_ids)) 1
   end;
 
-fun mk_mor_inv_tac alg_def mor_def set_natural's morEs map_comp_ids map_congLs =
+fun mk_mor_inv_tac alg_def mor_def set_natural's morEs map_comp_ids map_cong0Ls =
   let
     val fbetw_tac = EVERY' [rtac ballI, etac set_mp, etac imageI];
     fun Collect_tac set_natural' =
@@ -147,12 +147,12 @@
         FIRST' [rtac subset_UNIV,
           (EVERY' [rtac ord_eq_le_trans, rtac thm, rtac subset_trans,
             etac @{thm image_mono}, atac])]) set_natural';
-    fun mor_tac (set_natural', ((morE, map_comp_id), map_congL)) =
+    fun mor_tac (set_natural', ((morE, map_comp_id), map_cong0L)) =
       EVERY' [rtac ballI, ftac @{thm rev_bspec}, atac,
          REPEAT o eresolve_tac [CollectE, conjE], rtac sym, rtac trans, rtac sym,
          etac @{thm inverE}, etac bspec, rtac CollectI, Collect_tac set_natural',
          rtac trans, etac (morE RS arg_cong), rtac CollectI, Collect_tac set_natural',
-         rtac trans, rtac (map_comp_id RS arg_cong), rtac (map_congL RS arg_cong),
+         rtac trans, rtac (map_comp_id RS arg_cong), rtac (map_cong0L RS arg_cong),
          REPEAT_DETERM_N (length morEs) o
            (EVERY' [rtac subst, rtac @{thm inver_pointfree}, etac @{thm inver_mono}, atac])];
   in
@@ -162,7 +162,7 @@
     REPEAT o etac conjE THEN'
     rtac conjI THEN'
     CONJ_WRAP' (K fbetw_tac) set_natural's THEN'
-    CONJ_WRAP' mor_tac (set_natural's ~~ (morEs ~~ map_comp_ids ~~ map_congLs))) 1
+    CONJ_WRAP' mor_tac (set_natural's ~~ (morEs ~~ map_comp_ids ~~ map_cong0Ls))) 1
   end;
 
 fun mk_mor_str_tac ks mor_def =
@@ -436,7 +436,7 @@
   end;
 
 fun mk_init_unique_mor_tac m
-    alg_def alg_min_alg least_min_algs in_monos alg_sets morEs map_congs =
+    alg_def alg_min_alg least_min_algs in_monos alg_sets morEs map_cong0s =
   let
     val n = length least_min_algs;
     val ks = (1 upto n);
@@ -444,22 +444,22 @@
     fun mor_tac morE in_mono = EVERY' [etac morE, rtac set_mp, rtac in_mono,
       REPEAT_DETERM_N n o rtac @{thm Collect_restrict}, rtac CollectI,
       REPEAT_DETERM_N (m + n) o (TRY o rtac conjI THEN' atac)];
-    fun cong_tac map_cong = EVERY' [rtac (map_cong RS arg_cong),
+    fun cong_tac map_cong0 = EVERY' [rtac (map_cong0 RS arg_cong),
       REPEAT_DETERM_N m o rtac refl,
       REPEAT_DETERM_N n o (etac @{thm prop_restrict} THEN' atac)];
 
-    fun mk_alg_tac (alg_set, (in_mono, (morE, map_cong))) = EVERY' [rtac ballI, rtac CollectI,
+    fun mk_alg_tac (alg_set, (in_mono, (morE, map_cong0))) = EVERY' [rtac ballI, rtac CollectI,
       REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac conjI, rtac (alg_min_alg RS alg_set),
       REPEAT_DETERM_N m o rtac subset_UNIV,
       REPEAT_DETERM_N n o (etac subset_trans THEN' rtac @{thm Collect_restrict}),
       rtac trans, mor_tac morE in_mono,
-      rtac trans, cong_tac map_cong,
+      rtac trans, cong_tac map_cong0,
       rtac sym, mor_tac morE in_mono];
 
     fun mk_unique_tac (k, least_min_alg) =
       select_prem_tac n (etac @{thm prop_restrict}) k THEN' rtac least_min_alg THEN'
       stac alg_def THEN'
-      CONJ_WRAP' mk_alg_tac (alg_sets ~~ (in_monos ~~ (morEs ~~ map_congs)));
+      CONJ_WRAP' mk_alg_tac (alg_sets ~~ (in_monos ~~ (morEs ~~ map_cong0s)));
   in
     CONJ_WRAP' mk_unique_tac (ks ~~ least_min_algs) 1
   end;
@@ -514,9 +514,9 @@
     CONJ_WRAP' mk_unique type_defs 1
   end;
 
-fun mk_dtor_o_ctor_tac dtor_def foldx map_comp_id map_congL ctor_o_folds =
+fun mk_dtor_o_ctor_tac dtor_def foldx map_comp_id map_cong0L ctor_o_folds =
   EVERY' [stac dtor_def, rtac ext, rtac trans, rtac o_apply, rtac trans, rtac foldx,
-    rtac trans, rtac map_comp_id, rtac trans, rtac map_congL,
+    rtac trans, rtac map_comp_id, rtac trans, rtac map_cong0L,
     EVERY' (map (fn thm => rtac ballI THEN' rtac (trans OF [thm RS fun_cong, id_apply]))
       ctor_o_folds),
     rtac sym, rtac id_apply] 1;
@@ -575,16 +575,16 @@
       CONJ_WRAP' (K atac) ks] 1
   end;
 
-fun mk_map_tac m n foldx map_comp_id map_cong =
+fun mk_map_tac m n foldx map_comp_id map_cong0 =
   EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, rtac foldx, rtac trans, rtac o_apply,
-    rtac trans, rtac (map_comp_id RS arg_cong), rtac trans, rtac (map_cong RS arg_cong),
+    rtac trans, rtac (map_comp_id RS arg_cong), rtac trans, rtac (map_cong0 RS arg_cong),
     REPEAT_DETERM_N m o rtac refl,
     REPEAT_DETERM_N n o (EVERY' (map rtac [trans, o_apply, id_apply])),
     rtac sym, rtac o_apply] 1;
 
-fun mk_ctor_map_unique_tac m mor_def fold_unique_mor map_comp_ids map_congs =
+fun mk_ctor_map_unique_tac m mor_def fold_unique_mor map_comp_ids map_cong0s =
   let
-    val n = length map_congs;
+    val n = length map_cong0s;
     fun mk_mor (comp_id, cong) = EVERY' [rtac ballI, rtac trans, etac @{thm pointfreeE},
       rtac sym, rtac trans, rtac o_apply, rtac trans, rtac (comp_id RS arg_cong),
       rtac (cong RS arg_cong),
@@ -592,8 +592,8 @@
       REPEAT_DETERM_N n o (EVERY' (map rtac [trans, o_apply, id_apply]))];
   in
     EVERY' [rtac fold_unique_mor, rtac ssubst, rtac mor_def, rtac conjI,
-      CONJ_WRAP' (K (EVERY' [rtac ballI, rtac UNIV_I])) map_congs,
-      CONJ_WRAP' mk_mor (map_comp_ids ~~ map_congs)] 1
+      CONJ_WRAP' (K (EVERY' [rtac ballI, rtac UNIV_I])) map_cong0s,
+      CONJ_WRAP' mk_mor (map_comp_ids ~~ map_cong0s)] 1
   end;
 
 fun mk_set_tac foldx = EVERY' [rtac ext, rtac trans, rtac o_apply,
@@ -647,7 +647,7 @@
     (induct_tac THEN' EVERY' (map2 mk_set_nat ctor_sets set_bdss)) 1
   end;
 
-fun mk_mcong_tac induct_tac set_setsss map_congs ctor_maps {context = ctxt, prems = _} =
+fun mk_mcong_tac induct_tac set_setsss map_cong0s ctor_maps {context = ctxt, prems = _} =
   let
     fun use_asm thm = EVERY' [etac bspec, etac set_rev_mp, rtac thm];
 
@@ -655,14 +655,14 @@
       CONJ_WRAP' (fn thm =>
         EVERY' [rtac ballI, etac bspec, etac set_rev_mp, etac thm]) set_sets];
 
-    fun mk_map_cong ctor_map map_cong set_setss =
+    fun mk_map_cong0 ctor_map map_cong0 set_setss =
       EVERY' [rtac impI, REPEAT_DETERM o etac conjE,
-        rtac trans, rtac ctor_map, rtac trans, rtac (map_cong RS arg_cong),
+        rtac trans, rtac ctor_map, rtac trans, rtac (map_cong0 RS arg_cong),
         EVERY' (map use_asm (map hd set_setss)),
         EVERY' (map useIH (transpose (map tl set_setss))),
         rtac sym, rtac ctor_map];
   in
-    (induct_tac THEN' EVERY' (map3 mk_map_cong ctor_maps map_congs set_setsss)) 1
+    (induct_tac THEN' EVERY' (map3 mk_map_cong0 ctor_maps map_cong0s set_setsss)) 1
   end;
 
 fun mk_incl_min_alg_tac induct_tac set_setsss alg_sets alg_min_alg {context = ctxt, prems = _} =
@@ -775,7 +775,7 @@
           EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac ctor_set,
             REPEAT_DETERM_N n o etac UnE]))))] 1);
 
-fun mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong ctor_map ctor_sets ctor_inject
+fun mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong0 ctor_map ctor_sets ctor_inject
   ctor_dtor set_naturals ctor_set_incls ctor_set_set_inclss =
   let
     val m = length ctor_set_incls;
@@ -802,7 +802,7 @@
             rtac conjI, rtac refl, rtac refl])
         (in_Isrels ~~ (active_set_naturals ~~ ctor_set_set_inclss)),
         CONJ_WRAP' (fn conv =>
-          EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong,
+          EVERY' [rtac trans, rtac map_comp, 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,
@@ -827,7 +827,7 @@
         (ctor_sets ~~ passive_set_naturals),
         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_cong,
+          rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
           REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
           EVERY' (map (fn in_Isrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,
             dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Isrel RS iffD1),
diff -r e5ce85418346 -r 4c9f08836d87 src/HOL/BNF/Tools/bnf_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_tactics.ML	Wed Apr 24 14:14:36 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_tactics.ML	Wed Apr 24 14:15:01 2013 +0200
@@ -27,8 +27,8 @@
     thm -> thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
 
   val mk_map_comp_id_tac: thm -> tactic
-  val mk_map_cong_tac: int -> thm -> {prems: 'a, context: Proof.context} -> tactic
-  val mk_map_congL_tac: int -> thm -> thm -> tactic
+  val mk_map_cong0_tac: int -> thm -> {prems: 'a, context: Proof.context} -> tactic
+  val mk_map_cong0L_tac: int -> thm -> thm -> tactic
 end;
 
 structure BNF_Tactics : BNF_TACTICS =
@@ -101,12 +101,12 @@
 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_cong_tac m map_cong {context = ctxt, prems = _} =
-  EVERY' [rtac mp, rtac map_cong,
+fun mk_map_cong0_tac m map_cong0 {context = ctxt, prems = _} =
+  EVERY' [rtac mp, rtac map_cong0,
     CONJ_WRAP' (K (rtac ballI THEN' Goal.assume_rule_tac ctxt)) (1 upto m)] 1;
 
-fun mk_map_congL_tac passive map_cong map_id' =
-  (rtac trans THEN' rtac map_cong THEN' EVERY' (replicate passive (rtac refl))) 1 THEN
+fun mk_map_cong0L_tac passive map_cong0 map_id' =
+  (rtac trans THEN' rtac map_cong0 THEN' EVERY' (replicate passive (rtac refl))) 1 THEN
   REPEAT_DETERM (EVERY' [rtac trans, etac bspec, atac, rtac sym, rtac @{thm id_apply}] 1) THEN
   rtac map_id' 1;