# HG changeset patch
# User wenzelm
# Date 1377809597 -7200
# Node ID 2ad60808295c461844eceb4c6f7b0f437769ceec
# Parent  050d0bc9afa5e02e8e9738f46d476879bba140d5# Parent  64c31de7f21c100da49c107b699b0b83f91277cd
merged

diff -r 64c31de7f21c -r 2ad60808295c src/HOL/BNF/More_BNFs.thy
--- a/src/HOL/BNF/More_BNFs.thy	Thu Aug 29 22:40:50 2013 +0200
+++ b/src/HOL/BNF/More_BNFs.thy	Thu Aug 29 22:53:17 2013 +0200
@@ -227,7 +227,7 @@
 apply transfer apply simp
 done
 
-lemmas [simp] = fset.map_comp' fset.map_id' fset.set_map'
+lemmas [simp] = fset.map_comp fset.map_id fset.set_map'
 
 lemma fset_rel_fset: "set_rel \<chi> (fset A1) (fset A2) = fset_rel \<chi> A1 A2"
   unfolding fset_rel_def set_rel_def by auto
diff -r 64c31de7f21c -r 2ad60808295c src/HOL/BNF/Tools/bnf_comp.ML
--- a/src/HOL/BNF/Tools/bnf_comp.ML	Thu Aug 29 22:40:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML	Thu Aug 29 22:53:17 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 64c31de7f21c -r 2ad60808295c src/HOL/BNF/Tools/bnf_comp_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML	Thu Aug 29 22:40:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML	Thu Aug 29 22:53:17 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 64c31de7f21c -r 2ad60808295c src/HOL/BNF/Tools/bnf_def.ML
--- a/src/HOL/BNF/Tools/bnf_def.ML	Thu Aug 29 22:40:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Thu Aug 29 22:53:17 2013 +0200
@@ -50,13 +50,13 @@
   val in_cong_of_bnf: bnf -> thm
   val in_mono_of_bnf: bnf -> thm
   val in_rel_of_bnf: bnf -> thm
-  val map_comp'_of_bnf: bnf -> thm
+  val map_comp0_of_bnf: bnf -> thm
   val map_comp_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
   val map_id0_of_bnf: bnf -> thm
-  val map_id'_of_bnf: bnf -> thm
+  val map_id_of_bnf: bnf -> thm
   val map_transfer_of_bnf: bnf -> thm
   val map_wppull_of_bnf: bnf -> thm
   val map_wpull_of_bnf: bnf -> thm
@@ -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,
@@ -188,9 +188,9 @@
   in_cong: thm lazy,
   in_mono: thm lazy,
   in_rel: thm lazy,
-  map_comp': thm lazy,
+  map_comp: thm lazy,
   map_cong: thm lazy,
-  map_id': thm lazy,
+  map_id: thm lazy,
   map_transfer: thm lazy,
   map_wppull: thm lazy,
   rel_eq: thm lazy,
@@ -205,7 +205,7 @@
 };
 
 fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong in_mono in_rel
-    map_comp' map_cong map_id' map_transfer map_wppull rel_eq rel_flip set_map' rel_cong rel_mono
+    map_comp map_cong map_id map_transfer map_wppull rel_eq rel_flip set_map' rel_cong rel_mono
     rel_mono_strong rel_Grp rel_conversep rel_OO = {
   bd_Card_order = bd_Card_order,
   bd_Cinfinite = bd_Cinfinite,
@@ -215,9 +215,9 @@
   in_cong = in_cong,
   in_mono = in_mono,
   in_rel = in_rel,
-  map_comp' = map_comp',
+  map_comp = map_comp,
   map_cong = map_cong,
-  map_id' = map_id',
+  map_id = map_id,
   map_transfer = map_transfer,
   map_wppull = map_wppull,
   rel_eq = rel_eq,
@@ -239,9 +239,9 @@
   in_cong,
   in_mono,
   in_rel,
-  map_comp',
+  map_comp,
   map_cong,
-  map_id',
+  map_id,
   map_transfer,
   map_wppull,
   rel_eq,
@@ -261,9 +261,9 @@
     in_cong = Lazy.map f in_cong,
     in_mono = Lazy.map f in_mono,
     in_rel = Lazy.map f in_rel,
-    map_comp' = Lazy.map f map_comp',
+    map_comp = Lazy.map f map_comp,
     map_cong = Lazy.map f map_cong,
-    map_id' = Lazy.map f map_id',
+    map_id = Lazy.map f map_id,
     map_transfer = Lazy.map f map_transfer,
     map_wppull = Lazy.map f map_wppull,
     rel_eq = Lazy.map f rel_eq,
@@ -381,9 +381,9 @@
 val in_rel_of_bnf = Lazy.force o #in_rel o #facts o rep_bnf;
 val map_def_of_bnf = #map_def o #defs o rep_bnf;
 val map_id0_of_bnf = #map_id0 o #axioms o rep_bnf;
-val map_id'_of_bnf = Lazy.force o #map_id' o #facts o rep_bnf;
-val map_comp_of_bnf = #map_comp o #axioms o rep_bnf;
-val map_comp'_of_bnf = Lazy.force o #map_comp' o #facts o rep_bnf;
+val map_id_of_bnf = Lazy.force o #map_id o #facts 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;
 val map_transfer_of_bnf = Lazy.force o #map_transfer o #facts o rep_bnf;
@@ -509,9 +509,9 @@
 val in_monoN = "in_mono";
 val in_relN = "in_rel";
 val map_id0N = "map_id0";
-val map_id'N = "map_id'";
+val map_idN = "map_id";
+val map_comp0N = "map_comp0";
 val map_compN = "map_comp";
-val map_comp'N = "map_comp'";
 val map_cong0N = "map_cong0";
 val map_congN = "map_cong";
 val map_transferN = "map_transfer";
@@ -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]),
@@ -577,10 +577,10 @@
     #> (if fact_policy <> Dont_Note then
         let
           val notes =
-            [(map_comp'N, [Lazy.force (#map_comp' facts)], []),
+            [(map_compN, [Lazy.force (#map_comp facts)], []),
             (map_cong0N, [#map_cong0 axioms], []),
             (map_congN, [Lazy.force (#map_cong facts)], fundef_cong_attrs),
-            (map_id'N, [Lazy.force (#map_id' facts)], []),
+            (map_idN, [Lazy.force (#map_id facts)], []),
             (rel_eqN, [Lazy.force (#rel_eq facts)], []),
             (rel_flipN, [Lazy.force (#rel_flip facts)], []),
             (set_map'N, map Lazy.force (#set_map' facts), []),
@@ -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) =
@@ -1000,8 +1000,8 @@
 
         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_id = Lazy.lazy (fn () => mk_map_id (#map_id0 axioms));
+        val map_comp = Lazy.lazy (fn () => mk_map_comp (#map_comp0 axioms));
 
         fun mk_map_cong () =
           let
@@ -1049,7 +1049,7 @@
           in
             Goal.prove_sorry lthy [] [] in_bd_goal
               (mk_in_bd_tac live surj_imp_ordLeq_inst
-                (Lazy.force map_comp') (Lazy.force map_id') (#map_cong0 axioms)
+                (Lazy.force map_comp) (Lazy.force map_id) (#map_cong0 axioms)
                 (map Lazy.force set_map') (#set_bd axioms) (#bd_card_order axioms)
                 bd_Card_order bd_Cinfinite bd_Cnotzero)
             |> Thm.close_derivation
@@ -1087,7 +1087,7 @@
           in
             Goal.prove_sorry lthy [] [] goal
               (fn _ => mk_map_wppull_tac (#map_id0 axioms) (#map_cong0 axioms)
-                (#map_wpull axioms) (Lazy.force map_comp') (map Lazy.force set_map'))
+                (#map_wpull axioms) (Lazy.force map_comp) (map Lazy.force set_map'))
             |> Thm.close_derivation
           end;
 
@@ -1102,8 +1102,8 @@
             val goal = fold_rev Logic.all (As @ fs) (mk_Trueprop_eq (lhs, rhs));
           in
             Goal.prove_sorry lthy [] [] goal
-              (mk_rel_Grp_tac rel_OO_Grps (#map_id0 axioms) (#map_cong0 axioms) (Lazy.force map_id')
-                (Lazy.force map_comp') (map Lazy.force set_map'))
+              (mk_rel_Grp_tac rel_OO_Grps (#map_id0 axioms) (#map_cong0 axioms) (Lazy.force map_id)
+                (Lazy.force map_comp) (map Lazy.force set_map'))
             |> Thm.close_derivation
           end;
 
@@ -1155,7 +1155,7 @@
             val le_goal = fold_rev Logic.all Rs (HOLogic.mk_Trueprop (mk_leq lhs rhs));
             val le_thm = Goal.prove_sorry lthy [] [] le_goal
               (mk_rel_conversep_le_tac rel_OO_Grps (Lazy.force rel_eq) (#map_cong0 axioms)
-                (Lazy.force map_comp') (map Lazy.force set_map'))
+                (Lazy.force map_comp) (map Lazy.force set_map'))
               |> Thm.close_derivation
             val goal = fold_rev Logic.all Rs (mk_Trueprop_eq (lhs, rhs));
           in
@@ -1176,7 +1176,7 @@
           in
             Goal.prove_sorry lthy [] [] goal
               (mk_rel_OO_tac rel_OO_Grps (Lazy.force rel_eq) (#map_cong0 axioms)
-                (Lazy.force map_wppull) (Lazy.force map_comp') (map Lazy.force set_map'))
+                (Lazy.force map_wppull) (Lazy.force map_comp) (map Lazy.force set_map'))
             |> Thm.close_derivation
           end;
 
@@ -1245,7 +1245,7 @@
             Goal.prove_sorry lthy [] []
               (fold_rev Logic.all (transfer_domRs @ transfer_ranRs) concl)
               (mk_map_transfer_tac (Lazy.force rel_mono) (Lazy.force in_rel)
-                (map Lazy.force set_map') (#map_cong0 axioms) (Lazy.force map_comp'))
+                (map Lazy.force set_map') (#map_cong0 axioms) (Lazy.force map_comp))
             |> Thm.close_derivation
           end;
 
@@ -1254,7 +1254,7 @@
         val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def;
 
         val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong
-          in_mono in_rel map_comp' map_cong map_id' map_transfer map_wppull rel_eq rel_flip set_map'
+          in_mono in_rel map_comp map_cong map_id map_transfer map_wppull rel_eq rel_flip set_map'
           rel_cong rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO;
 
         val wits = map2 mk_witness bnf_wits wit_thms;
diff -r 64c31de7f21c -r 2ad60808295c src/HOL/BNF/Tools/bnf_def_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML	Thu Aug 29 22:40:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML	Thu Aug 29 22:53:17 2013 +0200
@@ -9,8 +9,8 @@
 signature BNF_DEF_TACTICS =
 sig
   val mk_collect_set_map_tac: thm list -> tactic
-  val mk_map_id': thm -> thm
-  val mk_map_comp': thm -> thm
+  val mk_map_id: thm -> thm
+  val mk_map_comp: thm -> thm
   val mk_map_cong_tac: Proof.context -> thm -> tactic
   val mk_in_mono_tac: int -> tactic
   val mk_map_wppull_tac: thm -> thm -> thm -> thm -> thm list -> tactic
@@ -45,8 +45,8 @@
 val ord_le_eq_trans = @{thm ord_le_eq_trans};
 val conversep_shift = @{thm conversep_le_swap} RS iffD1;
 
-fun mk_map_id' id = mk_trans (fun_cong OF [id]) @{thm id_apply};
-fun mk_map_comp' comp = @{thm o_eq_dest_lhs} OF [mk_sym comp];
+fun mk_map_id id = mk_trans (fun_cong OF [id]) @{thm id_apply};
+fun mk_map_comp comp = @{thm o_eq_dest_lhs} OF [mk_sym comp];
 fun mk_map_cong_tac ctxt cong0 =
   (hyp_subst_tac ctxt THEN' rtac cong0 THEN'
    REPEAT_DETERM o (dtac meta_spec THEN' etac meta_mp THEN' atac)) 1;
@@ -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,
@@ -113,7 +113,7 @@
               EVERY' [rtac ord_eq_le_trans, rtac thm, rtac @{thm image_subsetI},
                 rtac @{thm convol_mem_GrpI}, etac set_mp, atac])
             set_maps])
-          @{thms fst_convol snd_convol} [map_id', refl])] 1
+          @{thms fst_convol snd_convol} [map_id, refl])] 1
   end;
 
 fun mk_rel_eq_tac n rel_Grp rel_cong map_id0 =
@@ -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 = _} =
@@ -226,7 +226,7 @@
     EVERY' [rtac exI, rtac @{thm conjI[OF CollectI conjI[OF refl refl]]},
       CONJ_WRAP' (K (etac @{thm Collect_split_mono_strong} THEN' atac)) set_maps] 1;
 
-fun mk_map_transfer_tac rel_mono in_rel set_map's map_cong0 map_comp'
+fun mk_map_transfer_tac rel_mono in_rel set_map's map_cong0 map_comp
   {context = ctxt, prems = _} =
   let
     val n = length set_map's;
@@ -242,11 +242,11 @@
       set_map's,
       rtac conjI,
       EVERY' (map (fn convol =>
-        rtac (box_equals OF [map_cong0, map_comp' RS sym, map_comp' RS sym]) THEN'
+        rtac (box_equals OF [map_cong0, map_comp RS sym, map_comp RS sym]) THEN'
         REPEAT_DETERM_N n o rtac (convol RS fun_cong)) @{thms fst_convol snd_convol})])
   end;
 
-fun mk_in_bd_tac live surj_imp_ordLeq_inst map_comp' map_id' map_cong0 set_map's set_bds
+fun mk_in_bd_tac live surj_imp_ordLeq_inst map_comp map_id map_cong0 set_map's set_bds
   bd_card_order bd_Card_order bd_Cinfinite bd_Cnotzero {context = ctxt, prems = _} =
   if live = 0 then
     rtac @{thm ordLeq_transitive[OF ordLeq_csum2[OF card_of_Card_order]
@@ -294,7 +294,7 @@
         rtac sym,
         rtac (Drule.rotate_prems 1
            ((box_equals OF [map_cong0 OF replicate live @{thm If_the_inv_into_f_f},
-             map_comp' RS sym, map_id']) RSN (2, trans))),
+             map_comp RS sym, map_id]) RSN (2, trans))),
         REPEAT_DETERM_N (2 * live) o atac,
         REPEAT_DETERM_N live o rtac (@{thm prod.cases} RS trans),
         rtac refl,
@@ -305,7 +305,7 @@
         set_map's,
         rtac sym,
         rtac (box_equals OF [map_cong0 OF replicate live @{thm fun_cong[OF sum_case_o_inj(1)]},
-           map_comp' RS sym, map_id'])] 1
+           map_comp RS sym, map_id])] 1
   end;
 
 end;
diff -r 64c31de7f21c -r 2ad60808295c src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Aug 29 22:40:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Aug 29 22:53:17 2013 +0200
@@ -602,8 +602,8 @@
 
     val pre_map_defs = map map_def_of_bnf pre_bnfs;
     val pre_set_defss = map set_defs_of_bnf pre_bnfs;
-    val nesting_map_ids'' = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs;
-    val nested_map_ids'' = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs;
+    val nesting_map_id's = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs;
+    val nested_map_id's = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs;
     val nested_set_map's = maps set_map'_of_bnf nested_bnfs;
 
     val fp_b_names = map base_name_of_typ fpTs;
@@ -726,7 +726,7 @@
         val goalss = map5 (map4 o mk_goal fss) fiters xctrss fss xsss fxsss;
 
         val tacss =
-          map2 (map o mk_iter_tac pre_map_defs (nested_map_ids'' @ nesting_map_ids'') iter_defs)
+          map2 (map o mk_iter_tac pre_map_defs (nested_map_id's @ nesting_map_id's) iter_defs)
             ctor_iter_thms ctr_defss;
 
         fun prove goal tac =
@@ -763,7 +763,7 @@
 
     val pre_map_defs = map map_def_of_bnf pre_bnfs;
     val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
-    val nesting_map_ids'' = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs;
+    val nesting_map_id's = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nesting_bnfs;
     val nesting_rel_eqs = map rel_eq_of_bnf nesting_bnfs;
 
     val fp_b_names = map base_name_of_typ fpTs;
@@ -919,10 +919,10 @@
         val corec_goalss = map8 (map4 oooo mk_goal phss) cs cpss hcorecs ns kss ctrss mss cshsss';
 
         val unfold_tacss =
-          map3 (map oo mk_coiter_tac unfold_defs nesting_map_ids'')
+          map3 (map oo mk_coiter_tac unfold_defs nesting_map_id's)
             (map un_fold_of ctor_dtor_coiter_thmss) pre_map_defs ctr_defss;
         val corec_tacss =
-          map3 (map oo mk_coiter_tac corec_defs nesting_map_ids'')
+          map3 (map oo mk_coiter_tac corec_defs nesting_map_id's)
             (map co_rec_of ctor_dtor_coiter_thmss) pre_map_defs ctr_defss;
 
         fun prove goal tac =
diff -r 64c31de7f21c -r 2ad60808295c src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Thu Aug 29 22:40:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Thu Aug 29 22:53:17 2013 +0200
@@ -94,17 +94,17 @@
   @{thms comp_def convol_def fst_conv id_def prod_case_Pair_iden snd_conv
       split_conv unit_case_Unity} @ sum_prod_thms_map;
 
-fun mk_iter_tac pre_map_defs map_ids'' iter_defs ctor_iter ctr_def ctxt =
-  unfold_thms_tac ctxt (ctr_def :: ctor_iter :: iter_defs @ pre_map_defs @ map_ids'' @
+fun mk_iter_tac pre_map_defs map_id's iter_defs ctor_iter ctr_def ctxt =
+  unfold_thms_tac ctxt (ctr_def :: ctor_iter :: iter_defs @ pre_map_defs @ map_id's @
     iter_unfold_thms) THEN HEADGOAL (rtac refl);
 
 val coiter_unfold_thms = @{thms id_def} @ sum_prod_thms_map;
 
-fun mk_coiter_tac coiter_defs map_ids'' ctor_dtor_coiter pre_map_def ctr_def ctxt =
+fun mk_coiter_tac coiter_defs map_id's ctor_dtor_coiter pre_map_def ctr_def ctxt =
   unfold_thms_tac ctxt (ctr_def :: coiter_defs) THEN
   HEADGOAL (rtac (ctor_dtor_coiter RS trans) THEN'
     asm_simp_tac (put_simpset ss_if_True_False ctxt)) THEN_MAYBE
-  (unfold_thms_tac ctxt (pre_map_def :: map_ids'' @ coiter_unfold_thms) THEN
+  (unfold_thms_tac ctxt (pre_map_def :: map_id's @ coiter_unfold_thms) THEN
    HEADGOAL (rtac refl ORELSE' rtac (@{thm unit_eq} RS arg_cong)));
 
 fun mk_disc_coiter_iff_tac case_splits' coiters discs ctxt =
diff -r 64c31de7f21c -r 2ad60808295c src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Thu Aug 29 22:40:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Thu Aug 29 22:53:17 2013 +0200
@@ -214,12 +214,12 @@
     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_comp0s = map map_comp0_of_bnf bnfs;
+    val sym_map_comps = map mk_sym map_comp0s;
     val map_comps = map map_comp_of_bnf bnfs;
-    val sym_map_comps = map mk_sym map_comps;
-    val map_comp's = map map_comp'_of_bnf bnfs;
     val map_cong0s = map map_cong0_of_bnf bnfs;
     val map_id0s = map map_id0_of_bnf bnfs;
-    val map_id's = map map_id'_of_bnf bnfs;
+    val map_ids = map map_id_of_bnf bnfs;
     val map_wpulls = map map_wpull_of_bnf bnfs;
     val set_bdss = map set_bd_of_bnf bnfs;
     val set_map'ss = map set_map'_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,15 +246,15 @@
       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;
 
-    val map_comp_id_thms = map5 mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comp's;
+    val map_comp_id_thms = map5 mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comps;
 
     (*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_cong0L x mapAsAs sets map_cong0 map_id' =
+    fun mk_map_cong0L x mapAsAs sets map_cong0 map_id =
       let
         fun mk_prem set f z z' =
           HOLogic.mk_Trueprop
@@ -264,11 +264,11 @@
       in
         Goal.prove_sorry lthy [] []
           (fold_rev Logic.all (x :: self_fs) (Logic.list_implies (prems, goal)))
-          (K (mk_map_cong0L_tac m map_cong0 map_id'))
+          (K (mk_map_cong0L_tac m map_cong0 map_id))
         |> Thm.close_derivation
       end;
 
-    val map_cong0L_thms = map5 mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_id's;
+    val map_cong0L_thms = map5 mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_ids;
     val in_mono'_thms = map (fn thm =>
       (thm OF (replicate m subset_refl)) RS @{thm set_mp}) in_monos;
 
@@ -438,7 +438,7 @@
       in
         Goal.prove_sorry lthy [] []
           (fold_rev Logic.all (Bs @ ss @ Bs_copy) (Logic.list_implies (prems, concl)))
-          (K (mk_mor_incl_tac mor_def map_id's))
+          (K (mk_mor_incl_tac mor_def map_ids))
         |> Thm.close_derivation
       end;
 
@@ -809,7 +809,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_rel_tac lthy m bis_def rel_OO_Grps map_comp's map_cong0s set_map'ss))
+          (K (mk_bis_rel_tac lthy m bis_def rel_OO_Grps map_comps map_cong0s set_map'ss))
         |> Thm.close_derivation
       end;
 
@@ -2098,7 +2098,7 @@
       dtor_set_induct_thms, dtor_Jrel_thms, lthy) =
       if m = 0 then
         (timer, replicate n DEADID_bnf,
-        map_split (`(mk_pointfree lthy)) (map2 mk_dtor_map_DEADID_thm dtor_inject_thms map_id's),
+        map_split (`(mk_pointfree lthy)) (map2 mk_dtor_map_DEADID_thm dtor_inject_thms map_ids),
         replicate n [], [], map2 mk_dtor_Jrel_DEADID_thm dtor_inject_thms bnfs, lthy)
       else let
         val fTs = map2 (curry op -->) passiveAs passiveBs;
@@ -2184,16 +2184,16 @@
             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_cong0 =>
+              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_cong0))
+                  (K (mk_map_tac m n cT unfold map_comp map_cong0))
                 |> Thm.close_derivation)
-              goals cTs dtor_unfold_thms map_comp's map_cong0s;
+              goals cTs dtor_unfold_thms map_comps map_cong0s;
           in
             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;
 
@@ -2360,7 +2360,7 @@
 
             val thm = singleton (Proof_Context.export names_lthy lthy)
               (Goal.prove_sorry lthy [] [] goal
-              (K (mk_mcong_tac lthy m (rtac coinduct) map_comp's dtor_map_thms map_cong0s set_map'ss
+              (K (mk_mcong_tac lthy m (rtac coinduct) map_comps dtor_map_thms map_cong0s set_map'ss
               set_hset_thmss set_hset_hset_thmsss)))
               |> Thm.close_derivation
           in
@@ -2420,11 +2420,11 @@
               (Logic.mk_implies (wpull_prem, mor_pick));
           in
             (Goal.prove_sorry lthy [] [] fst_goal (mk_mor_thePull_fst_tac m mor_def map_wpull_thms
-              map_comp's pickWP_assms_tacs) |> Thm.close_derivation,
+              map_comps pickWP_assms_tacs) |> Thm.close_derivation,
             Goal.prove_sorry lthy [] [] snd_goal (mk_mor_thePull_snd_tac m mor_def map_wpull_thms
-              map_comp's pickWP_assms_tacs) |> Thm.close_derivation,
+              map_comps pickWP_assms_tacs) |> Thm.close_derivation,
             Goal.prove_sorry lthy [] [] pick_goal (mk_mor_thePull_pick_tac mor_def dtor_unfold_thms
-              map_comp's) |> Thm.close_derivation)
+              map_comps) |> Thm.close_derivation)
           end;
 
         val pick_col_thmss =
@@ -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,14 +2699,14 @@
               (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'
+            ks goals in_rels map_comps map_cong0s folded_dtor_map_thms folded_dtor_set_thmss'
               dtor_inject_thms dtor_ctor_thms set_map'ss dtor_set_incl_thmss
               dtor_set_set_incl_thmsss
           end;
@@ -2801,7 +2801,7 @@
             HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
               (map6 (mk_helper_coind_concl false)
               activeJphis Jzs Jz's_copy Jz's Jmap_snds zip_unfolds));
-          val helper_coind_tac = mk_rel_coinduct_coind_tac m dtor_map_coinduct_thm ks map_comp's
+          val helper_coind_tac = mk_rel_coinduct_coind_tac m dtor_map_coinduct_thm ks map_comps
             map_cong0s map_arg_cong_thms set_map'ss dtor_unfold_thms folded_dtor_map_thms;
           fun mk_helper_coind_thms vars concl =
             Goal.prove_sorry lthy [] []
diff -r 64c31de7f21c -r 2ad60808295c src/HOL/BNF/Tools/bnf_gfp_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Thu Aug 29 22:40:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Thu Aug 29 22:53:17 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
@@ -160,12 +160,12 @@
   etac bspec THEN'
   atac) 1;
 
-fun mk_mor_incl_tac mor_def map_id's =
+fun mk_mor_incl_tac mor_def map_ids =
   (stac mor_def THEN'
   rtac conjI THEN'
-  CONJ_WRAP' (K (EVERY' [rtac ballI, etac set_mp, stac id_apply, atac])) map_id's THEN'
+  CONJ_WRAP' (K (EVERY' [rtac ballI, etac set_mp, stac id_apply, atac])) map_ids THEN'
   CONJ_WRAP' (fn thm =>
-   (EVERY' [rtac ballI, rtac (thm RS trans), rtac sym, rtac (id_apply RS arg_cong)])) map_id's) 1;
+   (EVERY' [rtac ballI, rtac (thm RS trans), rtac sym, rtac (id_apply RS arg_cong)])) map_ids) 1;
 
 fun mk_mor_comp_tac mor_def mor_images morEs map_comp_ids =
   let
@@ -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,
@@ -1008,9 +1008,9 @@
         rtac CollectI, etac (refl RSN (2, @{thm subst_Pair}))]) ks] 1
   end;
 
-fun mk_map_tac m n cT unfold map_comp' map_cong0 =
+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_cong0,
+    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;
@@ -1034,36 +1034,36 @@
   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
+fun mk_mcong_tac ctxt m coinduct_tac map_comps dtor_maps map_cong0s set_mapss set_hsetss
   set_hset_hsetsss =
   let
-    val n = length map_comp's;
+    val n = length map_comps;
     val ks = 1 upto n;
   in
     EVERY' ([rtac rev_mp,
       coinduct_tac] @
-      maps (fn (((((map_comp'_trans, dtor_maps_trans), map_cong0), set_maps), set_hsets),
+      maps (fn (((((map_comp_trans, dtor_maps_trans), map_cong0), set_maps), set_hsets),
         set_hset_hsetss) =>
         [REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac ctxt, rtac exI, rtac conjI,
-         rtac conjI, rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong0,
+         rtac conjI, 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_cong0,
+         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),
@@ -1076,7 +1076,7 @@
              CONJ_WRAP' (fn set_hset_hset =>
                EVERY' [rtac ballI, etac bspec, etac set_hset_hset, atac]) set_hset_hsets])
            (drop m set_maps ~~ set_hset_hsetss)])
-        (map (fn th => th RS trans) map_comp's ~~ map (fn th => th RS trans) dtor_maps ~~
+        (map (fn th => th RS trans) map_comps ~~ map (fn th => th RS trans) dtor_maps ~~
           map_cong0s ~~ set_mapss ~~ set_hsetss ~~ set_hset_hsetsss) @
       [rtac impI,
        CONJ_WRAP' (fn k =>
@@ -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 64c31de7f21c -r 2ad60808295c src/HOL/BNF/Tools/bnf_lfp.ML
--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Thu Aug 29 22:40:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Thu Aug 29 22:53:17 2013 +0200
@@ -159,11 +159,11 @@
         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 map_comp's = map map_comp'_of_bnf bnfs;
+    val sym_map_comps = map (fn bnf => map_comp0_of_bnf bnf RS sym) bnfs;
+    val map_comps = map map_comp_of_bnf bnfs;
     val map_cong0s = map map_cong0_of_bnf bnfs;
     val map_id0s = map map_id0_of_bnf bnfs;
-    val map_id's = map map_id'_of_bnf bnfs;
+    val map_ids = map map_id_of_bnf bnfs;
     val map_wpulls = map map_wpull_of_bnf bnfs;
     val set_map'ss = map set_map'_of_bnf bnfs;
 
@@ -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,15 +203,15 @@
       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;
 
-    val map_comp_id_thms = map5 mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comp's;
+    val map_comp_id_thms = map5 mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comps;
 
     (*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_cong0L x mapAsAs sets map_cong0 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))));
@@ -220,11 +220,11 @@
       in
         Goal.prove_sorry lthy [] []
           (fold_rev Logic.all (x :: self_fs) (Logic.list_implies (prems, goal)))
-          (K (mk_map_cong0L_tac m map_cong0 map_id'))
+          (K (mk_map_cong0L_tac m map_cong0 map_id))
         |> Thm.close_derivation
       end;
 
-    val map_cong0L_thms = map5 mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_id's;
+    val map_cong0L_thms = map5 mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_ids;
     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;
 
@@ -389,7 +389,7 @@
       in
         Goal.prove_sorry lthy [] []
           (fold_rev Logic.all (Bs @ ss @ Bs_copy) (Logic.list_implies (prems, concl)))
-          (K (mk_mor_incl_tac mor_def map_id's))
+          (K (mk_mor_incl_tac mor_def map_ids))
         |> Thm.close_derivation
       end;
 
@@ -1405,7 +1405,7 @@
         ctor_Irel_thms, lthy) =
       if m = 0 then
         (timer, replicate n DEADID_bnf,
-        map_split (`(mk_pointfree lthy)) (map2 mk_ctor_map_DEADID_thm ctor_inject_thms map_id's),
+        map_split (`(mk_pointfree lthy)) (map2 mk_ctor_map_DEADID_thm ctor_inject_thms map_ids),
         replicate n [], map2 mk_ctor_Irel_DEADID_thm ctor_inject_thms bnfs, lthy)
       else let
         val fTs = map2 (curry op -->) passiveAs passiveBs;
@@ -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_comps 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,14 +1773,14 @@
               (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'
+            ks goals in_rels map_comps map_cong0s folded_ctor_map_thms folded_ctor_set_thmss'
               ctor_inject_thms ctor_dtor_thms set_map'ss ctor_set_incl_thmss
               ctor_set_set_incl_thmsss
           end;
diff -r 64c31de7f21c -r 2ad60808295c src/HOL/BNF/Tools/bnf_lfp_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Thu Aug 29 22:40:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Thu Aug 29 22:53:17 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
@@ -115,12 +115,12 @@
   etac bspec THEN'
   atac) 1;
 
-fun mk_mor_incl_tac mor_def map_id's =
+fun mk_mor_incl_tac mor_def map_ids =
   (stac mor_def THEN'
   rtac conjI THEN'
-  CONJ_WRAP' (K (EVERY' [rtac ballI, etac set_mp, stac id_apply, atac])) map_id's THEN'
+  CONJ_WRAP' (K (EVERY' [rtac ballI, etac set_mp, stac id_apply, atac])) map_ids THEN'
   CONJ_WRAP' (fn thm =>
-   (EVERY' [rtac ballI, rtac trans, rtac id_apply, stac thm, rtac refl])) map_id's) 1;
+   (EVERY' [rtac ballI, rtac trans, rtac id_apply, stac thm, rtac refl])) map_ids) 1;
 
 fun mk_mor_comp_tac mor_def set_map's map_comp_ids =
   let
@@ -710,18 +710,18 @@
     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_comp0s' = 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,
         rtac trans, rtac (simp RS arg_cong), rtac trans, rtac simp,
         rtac trans, rtac (comp RS arg_cong), rtac sym, rtac o_apply];
   in
-    (rtac sym THEN' rtac unique' THEN' EVERY' (map2 mk_comp map_comps' ctor_maps')) 1
+    (rtac sym THEN' rtac unique' THEN' EVERY' (map2 mk_comp map_comp0s' ctor_maps')) 1
   end;
 
 fun mk_set_map_tac set_nat =
@@ -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 64c31de7f21c -r 2ad60808295c src/HOL/BNF/Tools/bnf_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_tactics.ML	Thu Aug 29 22:40:50 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_tactics.ML	Thu Aug 29 22:53:17 2013 +0200
@@ -106,16 +106,16 @@
       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,
     CONJ_WRAP' (K (rtac ballI THEN' Goal.assume_rule_tac ctxt)) (1 upto m)] 1;
 
-fun mk_map_cong0L_tac passive map_cong0 map_id' =
+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;
+  rtac map_id 1;
 
 end;
diff -r 64c31de7f21c -r 2ad60808295c src/HOL/Tools/Lifting/lifting_info.ML
--- a/src/HOL/Tools/Lifting/lifting_info.ML	Thu Aug 29 22:40:50 2013 +0200
+++ b/src/HOL/Tools/Lifting/lifting_info.ML	Thu Aug 29 22:53:17 2013 +0200
@@ -179,7 +179,7 @@
     val (_, qtyp) = quot_thm_rty_qty quot_thm
     val qty_full_name = (fst o dest_Type) qtyp
     val symtab = get_quotients' ctxt
-    fun compare_data (_, data) = Thm.eq_thm_prop (#quot_thm data, quot_thm)
+    fun compare_data (_, data:quotient) = Thm.eq_thm_prop (#quot_thm data, quot_thm)
   in
     if Symtab.member compare_data symtab (qty_full_name, quot_thm)
       then Data.map (map_quotients (Symtab.delete qty_full_name)) ctxt