renamed BNF axiom

--- a/src/HOL/BNF/Tools/bnf_comp.ML	Thu Aug 29 22:39:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML	Thu Aug 29 22:56:39 2013 +0200
@@ -157,12 +157,12 @@
       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_comp0_of_bnf outer) (map_cong0_of_bnf outer)
+    fun mk_single_set_map0_tac i _ =
+      mk_comp_set_map0_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);
+        (map ((fn thms => nth thms i) o set_map0_of_bnf) inners);
 
-    val set_map_tacs = map mk_single_set_map_tac (0 upto ilive - 1);
+    val set_map0_tacs = map mk_single_set_map0_tac (0 upto ilive - 1);
 
     fun bd_card_order_tac _ =
       mk_comp_bd_card_order_tac (map bd_card_order_of_bnf inners) (bd_card_order_of_bnf outer);
@@ -233,7 +233,7 @@
         rtac thm 1
       end;
 
-    val tacs = zip_axioms map_id0_tac map_comp0_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_map0_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;
@@ -306,7 +306,7 @@
       rtac refl 1;
     fun map_cong0_tac {context = ctxt, prems = _} =
       mk_kill_map_cong0_tac ctxt n (live - n) (map_cong0_of_bnf bnf);
-    val set_map_tacs = map (fn thm => fn _ => rtac thm 1) (drop n (set_map_of_bnf bnf));
+    val set_map0_tacs = map (fn thm => fn _ => rtac thm 1) (drop n (set_map0_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);
     val set_bd_tacs =
@@ -339,7 +339,7 @@
         rtac thm 1
       end;
 
-    val tacs = zip_axioms map_id0_tac map_comp0_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_map0_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;
@@ -396,12 +396,12 @@
       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);
-    val set_map_tacs =
+    val set_map0_tacs =
       if Config.get lthy quick_and_dirty then
         replicate (n + live) (K all_tac)
       else
         replicate n (K empty_natural_tac) @
-        map (fn thm => fn _ => rtac thm 1) (set_map_of_bnf bnf);
+        map (fn thm => fn _ => rtac thm 1) (set_map0_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;
     val set_bd_tacs =
@@ -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_comp0_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_map0_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);
@@ -478,7 +478,7 @@
     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));
+    val set_map0_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_map0_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;
     val set_bd_tacs = permute (map (fn thm => fn _ => rtac thm 1) (set_bd_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_comp0_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_map0_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);
@@ -631,7 +631,7 @@
       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_comp0_of_bnf bnf))
-      (mk_tac (map_cong0_of_bnf bnf)) (map mk_tac (set_map_of_bnf bnf))
+      (mk_tac (map_cong0_of_bnf bnf)) (map mk_tac (set_map0_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))
       (mk_tac (rel_OO_Grp_of_bnf bnf));

--- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML	Thu Aug 29 22:39:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML	Thu Aug 29 22:56:39 2013 +0200
@@ -16,7 +16,7 @@
   val mk_comp_map_id0_tac: thm -> thm -> thm list -> tactic
   val mk_comp_set_alt_tac: Proof.context -> thm -> tactic
   val mk_comp_set_bd_tac: Proof.context -> thm -> thm list -> tactic
-  val mk_comp_set_map_tac: thm -> thm -> thm -> thm list -> tactic
+  val mk_comp_set_map0_tac: thm -> thm -> thm -> thm list -> tactic
   val mk_comp_wit_tac: Proof.context -> thm list -> thm -> thm list -> tactic
 
   val mk_kill_bd_card_order_tac: int -> thm -> tactic
@@ -67,21 +67,21 @@
     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_comp0 Gmap_cong0 Gset_map set_maps =
+fun mk_comp_set_map0_tac Gmap_comp0 Gmap_cong0 Gset_map0 set_map0s =
   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_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,
+     map (fn thm => rtac (thm RS fun_cong)) set_map0s @
+     [rtac (Gset_map0 RS o_eq_dest_lhs), rtac sym, rtac trans_o_apply,
      rtac trans_image_cong_o_apply, rtac trans_image_cong_o_apply,
-     rtac (@{thm image_cong} OF [Gset_map RS o_eq_dest_lhs RS arg_cong_Union, refl] RS trans),
+     rtac (@{thm image_cong} OF [Gset_map0 RS o_eq_dest_lhs RS arg_cong_Union, refl] RS trans),
      rtac @{thm trans[OF comp_eq_dest[OF Union_natural[symmetric]]]}, rtac arg_cong_Union,
      rtac @{thm trans[OF o_eq_dest_lhs[OF image_o_collect[symmetric]]]},
      rtac @{thm fun_cong[OF arg_cong[of _ _ collect]]}] @
-     [REPEAT_DETERM_N (length set_maps) o EVERY' [rtac @{thm trans[OF image_insert]},
+     [REPEAT_DETERM_N (length set_map0s) o EVERY' [rtac @{thm trans[OF image_insert]},
         rtac @{thm arg_cong2[of _ _ _ _ insert]}, rtac ext, rtac trans_o_apply,
         rtac trans_image_cong_o_apply, rtac @{thm trans[OF image_image]},
         rtac @{thm sym[OF trans[OF o_apply]]}, rtac @{thm image_cong[OF refl o_apply]}],

--- a/src/HOL/BNF/Tools/bnf_def.ML	Thu Aug 29 22:39:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Thu Aug 29 22:56:39 2013 +0200
@@ -72,8 +72,8 @@
   val rel_flip_of_bnf: bnf -> thm
   val set_bd_of_bnf: bnf -> thm list
   val set_defs_of_bnf: bnf -> thm list
+  val set_map0_of_bnf: bnf -> thm list
   val set_map'_of_bnf: bnf -> thm list
-  val set_map_of_bnf: bnf -> thm list
   val wit_thms_of_bnf: bnf -> thm list
   val wit_thmss_of_bnf: bnf -> thm list list
 
@@ -116,7 +116,7 @@
   map_id0: thm,
   map_comp0: thm,
   map_cong0: thm,
-  set_map: thm list,
+  set_map0: thm list,
   bd_card_order: thm,
   bd_cinfinite: thm,
   set_bd: thm list,
@@ -124,8 +124,8 @@
   rel_OO_Grp: thm
 };
 
-fun mk_axioms' ((((((((id, comp), cong), nat), c_o), cinf), set_bd), wpull), rel) =
-  {map_id0 = id, map_comp0 = comp, map_cong0 = cong, set_map = nat, bd_card_order = c_o,
+fun mk_axioms' ((((((((id, comp), cong), map), c_o), cinf), set_bd), wpull), rel) =
+  {map_id0 = id, map_comp0 = comp, map_cong0 = cong, set_map0 = map, 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
@@ -144,20 +144,20 @@
   ||> the_single
   |> mk_axioms';
 
-fun zip_axioms mid mcomp mcong snat bdco bdinf sbd wpull rel =
-  [mid, mcomp, mcong] @ snat @ [bdco, bdinf] @ sbd @ [wpull, rel];
+fun zip_axioms mid mcomp mcong smap bdco bdinf sbd wpull rel =
+  [mid, mcomp, mcong] @ smap @ [bdco, bdinf] @ sbd @ [wpull, rel];
 
-fun dest_axioms {map_id0, map_comp0, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd,
+fun dest_axioms {map_id0, map_comp0, map_cong0, set_map0, bd_card_order, bd_cinfinite, set_bd,
   map_wpull, rel_OO_Grp} =
-  zip_axioms map_id0 map_comp0 map_cong0 set_map bd_card_order bd_cinfinite set_bd map_wpull
+  zip_axioms map_id0 map_comp0 map_cong0 set_map0 bd_card_order bd_cinfinite set_bd map_wpull
     rel_OO_Grp;
 
-fun map_axioms f {map_id0, map_comp0, map_cong0, set_map, bd_card_order, bd_cinfinite, set_bd,
+fun map_axioms f {map_id0, map_comp0, map_cong0, set_map0, bd_card_order, bd_cinfinite, set_bd,
   map_wpull, rel_OO_Grp} =
   {map_id0 = f map_id0,
     map_comp0 = f map_comp0,
     map_cong0 = f map_cong0,
-    set_map = map f set_map,
+    set_map0 = map f set_map0,
     bd_card_order = f bd_card_order,
     bd_cinfinite = f bd_cinfinite,
     set_bd = map f set_bd,
@@ -394,7 +394,7 @@
 val rel_flip_of_bnf = Lazy.force o #rel_flip o #facts o rep_bnf;
 val set_bd_of_bnf = #set_bd o #axioms o rep_bnf;
 val set_defs_of_bnf = #set_defs o #defs o rep_bnf;
-val set_map_of_bnf = #set_map o #axioms o rep_bnf;
+val set_map0_of_bnf = #set_map0 o #axioms o rep_bnf;
 val set_map'_of_bnf = map Lazy.force o #set_map' o #facts o rep_bnf;
 val rel_cong_of_bnf = Lazy.force o #rel_cong o #facts o rep_bnf;
 val rel_mono_of_bnf = Lazy.force o #rel_mono o #facts o rep_bnf;
@@ -518,7 +518,7 @@
 val map_wpullN = "map_wpull";
 val rel_eqN = "rel_eq";
 val rel_flipN = "rel_flip";
-val set_mapN = "set_map";
+val set_map0N = "set_map0";
 val set_map'N = "set_map'";
 val set_bdN = "set_bd";
 val rel_GrpN = "rel_Grp";
@@ -563,7 +563,7 @@
             (map_transferN, [Lazy.force (#map_transfer facts)]),
             (map_wpullN, [#map_wpull axioms]),
             (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)]),
-            (set_mapN, #set_map axioms),
+            (set_map0N, #set_map0 axioms),
             (set_bdN, #set_bd axioms)] @
             (witNs ~~ wit_thmss_of_bnf bnf)
             |> map (fn (thmN, thms) =>
@@ -873,7 +873,7 @@
         fold_rev Logic.all (x :: fs @ fs_copy) (Logic.list_implies (prems, eq))
       end;
 
-    val set_maps_goal =
+    val set_map0s_goal =
       let
         fun mk_goal setA setB f =
           let
@@ -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_comp0_goal map_cong0_goal set_maps_goal
+    val goals = zip_axioms map_id0_goal map_comp0_goal map_cong0_goal set_map0s_goal
       card_order_bd_goal cinfinite_bd_goal set_bds_goal map_wpull_goal rel_OO_Grp_goal;
 
     fun mk_wit_goals (I, wit) =
@@ -965,7 +965,7 @@
             (*collect {set1 ... setm} o map f1 ... fm = collect {f1` o set1 ... fm` o setm}*)
             val goal = fold_rev Logic.all hs (mk_Trueprop_eq (collect_map, image_collect));
           in
-            Goal.prove_sorry lthy [] [] goal (K (mk_collect_set_map_tac (#set_map axioms)))
+            Goal.prove_sorry lthy [] [] goal (K (mk_collect_set_map_tac (#set_map0 axioms)))
             |> Thm.close_derivation
           end;
 
@@ -1018,7 +1018,7 @@
 
         val map_cong = Lazy.lazy mk_map_cong;
 
-        val set_map' = map (fn thm => Lazy.lazy (fn () => mk_set_map' thm)) (#set_map axioms);
+        val set_map' = map (fn thm => Lazy.lazy (fn () => mk_set_map' thm)) (#set_map0 axioms);
 
         fun mk_in_bd () =
           let
@@ -1335,12 +1335,12 @@
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "print_bnfs"}
-    "print all BNFs (bounded natural functors)"
+    "print all bounded natural functors"
     (Scan.succeed (Toplevel.keep (print_bnfs o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.local_theory_to_proof @{command_spec "bnf"}
-    "register a type as a BNF (bounded natural functor)"
+    "register a type as a bounded natural functor"
     ((parse_opt_binding_colon -- Parse.term --
        (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- Parse.term --
        (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- Scan.option Parse.term)

--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML	Thu Aug 29 22:39:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML	Thu Aug 29 22:56:39 2013 +0200
@@ -50,7 +50,7 @@
 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;
-fun mk_set_map' set_map = set_map RS @{thm comp_eq_dest};
+fun mk_set_map' set_map0 = set_map0 RS @{thm comp_eq_dest};
 fun mk_in_mono_tac n = if n = 0 then rtac subset_UNIV 1
   else (rtac subsetI THEN'
   rtac CollectI) 1 THEN
@@ -59,15 +59,15 @@
     ((rtac conjI THEN' etac subset_trans THEN' atac) 1) THEN
   (etac subset_trans THEN' atac) 1;
 
-fun mk_collect_set_map_tac set_maps =
+fun mk_collect_set_map_tac set_map0s =
   (rtac (@{thm collect_o} RS trans) THEN' rtac @{thm arg_cong[of _ _ collect]} THEN'
-  EVERY' (map (fn set_map =>
+  EVERY' (map (fn set_map0 =>
     rtac (mk_trans @{thm image_insert} @{thm arg_cong2[of _ _ _ _ insert]}) THEN'
-    rtac set_map) set_maps) THEN'
+    rtac set_map0) set_map0s) THEN'
   rtac @{thm image_empty}) 1;
 
-fun mk_map_wppull_tac map_id0 map_cong0 map_wpull map_comp0 set_maps =
-  if null set_maps then
+fun mk_map_wppull_tac map_id0 map_cong0 map_wpull map_comp0 set_map0s =
+  if null set_map0s 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},
     REPEAT_DETERM o etac exE, rtac @{thm wpull_wppull}, rtac map_wpull,
@@ -75,20 +75,20 @@
     REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac conjI, rtac CollectI,
     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,
+      set_map0s,
     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),
+      REPEAT_DETERM_N (length set_map0s) 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_comp0 set_maps
+fun mk_rel_Grp_tac rel_OO_Grps map_id0 map_cong0 map_id map_comp0 set_map0s
   {context = ctxt, prems = _} =
   let
-    val n = length set_maps;
+    val n = length set_map0s;
     val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac else rtac (hd rel_OO_Grps RS trans);
   in
-    if null set_maps then
+    if null set_map0s then
       unfold_thms_tac ctxt ((map_id0 RS @{thm Grp_UNIV_id}) :: rel_OO_Grps) THEN
       rtac @{thm Grp_UNIV_idI[OF refl]} 1
     else
@@ -100,7 +100,7 @@
         rtac CollectI,
         CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans),
           rtac @{thm image_subsetI}, rtac @{thm Collect_split_Grp_inD}, etac @{thm set_mp}, atac])
-        set_maps,
+        set_map0s,
         rtac @{thm predicate2I}, REPEAT_DETERM o eresolve_tac [@{thm GrpE}, exE, conjE],
         hyp_subst_tac ctxt,
         rtac @{thm relcomppI}, rtac @{thm conversepI},
@@ -112,7 +112,7 @@
             CONJ_WRAP' (fn thm =>
               EVERY' [rtac ord_eq_le_trans, rtac thm, rtac @{thm image_subsetI},
                 rtac @{thm convol_mem_GrpI}, etac set_mp, atac])
-            set_maps])
+            set_map0s])
           @{thms fst_convol snd_convol} [map_id, refl])] 1
   end;
 
@@ -135,15 +135,15 @@
       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_comp0 set_maps
+fun mk_rel_conversep_le_tac rel_OO_Grps rel_eq map_cong0 map_comp0 set_map0s
   {context = ctxt, prems = _} =
   let
-    val n = length set_maps;
+    val n = length set_map0s;
     val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac
       else rtac (hd rel_OO_Grps RS ord_eq_le_trans) THEN'
         rtac (hd rel_OO_Grps RS sym RS @{thm arg_cong[of _ _ conversep]} RSN (2, ord_le_eq_trans));
   in
-    if null set_maps then rtac (rel_eq RS @{thm leq_conversepI}) 1
+    if null set_map0s then rtac (rel_eq RS @{thm leq_conversepI}) 1
     else
       EVERY' [rel_OO_Grps_tac, rtac @{thm predicate2I},
         REPEAT_DETERM o
@@ -153,7 +153,7 @@
           rtac map_cong0, REPEAT_DETERM_N n o rtac thm,
           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
+            etac @{thm flip_pred}]) set_map0s]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1
   end;
 
 fun mk_rel_conversep_tac le_conversep rel_mono =
@@ -161,19 +161,19 @@
     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_comp0 set_maps
+fun mk_rel_OO_tac rel_OO_Grps rel_eq map_cong0 map_wppull map_comp0 set_map0s
   {context = ctxt, prems = _} =
   let
-    val n = length set_maps;
+    val n = length set_map0s;
     fun in_tac nthO_in = rtac CollectI THEN'
         CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans),
-          rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_maps;
+          rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_map0s;
     val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac
       else rtac (hd rel_OO_Grps RS trans) THEN'
         rtac (@{thm arg_cong2[of _ _ _ _ "op OO"]} OF (replicate 2 (hd rel_OO_Grps RS sym)) RSN
           (2, trans));
   in
-    if null set_maps then rtac (rel_eq RS @{thm eq_OOI}) 1
+    if null set_map0s then rtac (rel_eq RS @{thm eq_OOI}) 1
     else
       EVERY' [rel_OO_Grps_tac, rtac @{thm antisym}, rtac @{thm predicate2I},
         REPEAT_DETERM o
@@ -200,7 +200,7 @@
         REPEAT_DETERM o eresolve_tac [@{thm relcomppE}, @{thm conversepE}, @{thm GrpE}],
         hyp_subst_tac ctxt,
         rtac allE, rtac subst, rtac @{thm wppull_def}, rtac map_wppull,
-        CONJ_WRAP' (K (rtac @{thm wppull_fstOp_sndOp})) set_maps,
+        CONJ_WRAP' (K (rtac @{thm wppull_fstOp_sndOp})) set_map0s,
         etac allE, etac impE, etac conjI, etac conjI, etac sym,
         REPEAT_DETERM o eresolve_tac [bexE, conjE],
         rtac @{thm relcomppI}, rtac @{thm conversepI},
@@ -216,15 +216,15 @@
     REPEAT_DETERM o eresolve_tac [exE, conjE], rtac @{thm relcomppI}, rtac @{thm conversepI},
     etac @{thm GrpI}, atac, etac @{thm GrpI}, atac] 1;
 
-fun mk_rel_mono_strong_tac in_rel set_maps {context = ctxt, prems = _} =
-  if null set_maps then atac 1
+fun mk_rel_mono_strong_tac in_rel set_map0s {context = ctxt, prems = _} =
+  if null set_map0s then atac 1
   else
     unfold_tac [in_rel] ctxt THEN
     REPEAT_DETERM (eresolve_tac [exE, CollectE, conjE] 1) THEN
     hyp_subst_tac ctxt 1 THEN
-    unfold_tac set_maps ctxt THEN
+    unfold_tac set_map0s ctxt THEN
     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;
+      CONJ_WRAP' (K (etac @{thm Collect_split_mono_strong} THEN' atac)) set_map0s] 1;
 
 fun mk_map_transfer_tac rel_mono in_rel set_map's map_cong0 map_comp
   {context = ctxt, prems = _} =

--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Thu Aug 29 22:39:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Thu Aug 29 22:56:39 2013 +0200
@@ -2462,7 +2462,7 @@
         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);
+          map2 (map2 (K oo mk_set_map0_tac)) hset_defss (transpose col_natural_thmss);
 
         val bd_co_tacs = replicate n (K (mk_bd_card_order_tac sbd_card_order));
         val bd_cinf_tacs = replicate n (K (mk_bd_cinfinite_tac sbd_Cinfinite));
@@ -2701,10 +2701,10 @@
           in
             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 =>
+              fn set_map0s => 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_comp0 map_cong0 dtor_map dtor_sets
-                  dtor_inject dtor_ctor set_maps dtor_set_incls dtor_set_set_inclss))
+                  dtor_inject dtor_ctor set_map0s dtor_set_incls dtor_set_set_inclss))
               |> Thm.close_derivation)
             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

--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Thu Aug 29 22:39:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Thu Aug 29 22:56:39 2013 +0200
@@ -107,7 +107,7 @@
   val mk_set_incl_hin_tac: thm list -> tactic
   val mk_set_incl_hset_tac: thm -> thm -> tactic
   val mk_set_le_tac: int -> thm -> thm list -> thm list list -> tactic
-  val mk_set_map_tac: thm -> thm -> tactic
+  val mk_set_map0_tac: thm -> thm -> tactic
   val mk_set_rv_Lev_tac: Proof.context -> int -> cterm option list -> thm list -> thm list ->
     thm list -> thm list -> thm list list -> thm list list -> tactic
   val mk_unfold_unique_mor_tac: thm list -> thm -> thm -> thm list -> tactic
@@ -234,34 +234,34 @@
     EVERY' (replicate ((n + 1) * n) (Goal.assume_rule_tac ctxt)), rtac impI,
     REPEAT_DETERM o eresolve_tac [allE, conjE], atac])) hset_defs) 1
 
-fun mk_mor_hset_rec_tac m n cts j rec_0s rec_Sucs morEs set_mapss coalg_setss =
+fun mk_mor_hset_rec_tac m n cts j rec_0s rec_Sucs morEs set_map0ss coalg_setss =
   EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
     REPEAT_DETERM o rtac allI,
     CONJ_WRAP' (fn thm => EVERY' (map rtac [impI, thm RS trans, thm RS sym])) rec_0s,
     REPEAT_DETERM o rtac allI,
     CONJ_WRAP'
-      (fn (rec_Suc, (morE, ((passive_set_maps, active_set_maps), coalg_sets))) =>
+      (fn (rec_Suc, (morE, ((passive_set_map0s, active_set_map0s), coalg_sets))) =>
         EVERY' [rtac impI, rtac (rec_Suc RS trans), rtac (rec_Suc RS trans RS sym),
           if m = 0 then K all_tac
           else EVERY' [rtac Un_cong, rtac box_equals,
-            rtac (nth passive_set_maps (j - 1) RS sym),
+            rtac (nth passive_set_map0s (j - 1) RS sym),
             rtac trans_fun_cong_image_id_id_apply, etac (morE RS arg_cong), atac],
           CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 Un_cong))
-            (fn (i, (set_map, coalg_set)) =>
+            (fn (i, (set_map0, coalg_set)) =>
               EVERY' [rtac sym, rtac trans, rtac (refl RSN (2, @{thm UN_cong})),
-                etac (morE RS sym RS arg_cong RS trans), atac, rtac set_map,
+                etac (morE RS sym RS arg_cong RS trans), atac, rtac set_map0,
                 rtac (@{thm UN_simps(10)} RS trans), rtac (refl RS @{thm UN_cong}),
                 ftac coalg_set, atac, dtac set_mp, atac, rtac mp, rtac (mk_conjunctN n i),
                 REPEAT_DETERM o etac allE, atac, atac])
-            (rev ((1 upto n) ~~ (active_set_maps ~~ coalg_sets)))])
-      (rec_Sucs ~~ (morEs ~~ (map (chop m) set_mapss ~~ map (drop m) coalg_setss)))] 1;
+            (rev ((1 upto n) ~~ (active_set_map0s ~~ coalg_sets)))])
+      (rec_Sucs ~~ (morEs ~~ (map (chop m) set_map0ss ~~ map (drop m) coalg_setss)))] 1;
 
-fun mk_bis_rel_tac ctxt m bis_def rel_OO_Grps map_comp0s map_cong0s set_mapss =
+fun mk_bis_rel_tac ctxt m bis_def rel_OO_Grps map_comp0s map_cong0s set_map0ss =
   let
     val n = length rel_OO_Grps;
-    val thms = ((1 upto n) ~~ map_comp0s ~~ map_cong0s ~~ set_mapss ~~ rel_OO_Grps);
+    val thms = ((1 upto n) ~~ map_comp0s ~~ map_cong0s ~~ set_map0ss ~~ rel_OO_Grps);
 
-    fun mk_if_tac ((((i, map_comp0), map_cong0), set_maps), rel_OO_Grp) =
+    fun mk_if_tac ((((i, map_comp0), map_cong0), set_map0s), 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}),
@@ -278,10 +278,10 @@
                 etac @{thm Collect_split_in_relI[OF Id_onI]}]
               else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm,
                 rtac trans_fun_cong_image_id_id_apply, etac @{thm Collect_split_in_rel_leI}])
-            (1 upto (m + n) ~~ set_maps)])
+            (1 upto (m + n) ~~ set_map0s)])
           @{thms fst_diag_id snd_diag_id})];
 
-    fun mk_only_if_tac ((((i, map_comp0), map_cong0), set_maps), rel_OO_Grp) =
+    fun mk_only_if_tac ((((i, map_comp0), map_cong0), set_map0s), 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}),
@@ -304,7 +304,7 @@
             rtac @{thm Id_on_fst}, etac set_mp, atac]
           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_maps)];
+        (1 upto (m + n) ~~ set_map0s)];
   in
     EVERY' [rtac (bis_def RS trans),
       rtac iffI, etac conjE, etac conjI, CONJ_WRAP' mk_if_tac thms,
@@ -399,7 +399,7 @@
     rtac incl_lsbis, rtac bis_O, rtac sbis_lsbis, rtac sbis_lsbis,
     etac @{thm relcompI}, atac] 1;
 
-fun mk_coalgT_tac m defs strT_defs set_mapss {context = ctxt, prems = _} =
+fun mk_coalgT_tac m defs strT_defs set_map0ss {context = ctxt, prems = _} =
   let
     val n = length strT_defs;
     val ks = 1 upto n;
@@ -444,7 +444,7 @@
             rtac (@{thm append_Nil} RS sym RS arg_cong)])) ks]) (ks ~~ active_sets)];
   in
     unfold_thms_tac ctxt defs THEN
-    CONJ_WRAP' coalg_tac (ks ~~ (map (chop m) set_mapss ~~ strT_defs)) 1
+    CONJ_WRAP' coalg_tac (ks ~~ (map (chop m) set_map0ss ~~ strT_defs)) 1
   end;
 
 fun mk_Lev_sbd_tac ctxt cts Lev_0s Lev_Sucs to_sbdss =
@@ -685,14 +685,14 @@
 
 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_mapss coalg_setss
+  prefCl_Levs rv_lastss set_rv_Levsss set_Levsss set_image_Levsss set_map0ss coalg_setss
   map_comp_ids map_cong0s map_arg_congs {context = ctxt, prems = _} =
   let
     val n = length beh_defs;
     val ks = 1 upto n;
 
     fun fbetw_tac (i, (carT_def, (isNode_def, (Lev_0, (rv_Nil, (Lev_sbd,
-      ((length_Lev, length_Lev'), (prefCl_Lev, (rv_lasts, (set_maps,
+      ((length_Lev, length_Lev'), (prefCl_Lev, (rv_lasts, (set_map0s,
         (coalg_sets, (set_rv_Levss, (set_Levss, set_image_Levss))))))))))))) =
       EVERY' [rtac ballI, rtac (carT_def RS equalityD2 RS set_mp),
         rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, rtac conjI,
@@ -708,29 +708,29 @@
         rtac conjI,
           rtac ballI, etac @{thm UN_E}, rtac conjI,
           if n = 1 then K all_tac else rtac (mk_sumEN n),
-          EVERY' (map6 (fn i => fn isNode_def => fn set_maps =>
+          EVERY' (map6 (fn i => fn isNode_def => fn set_map0s =>
             fn set_rv_Levs => fn set_Levs => fn set_image_Levs =>
             EVERY' [rtac (mk_disjIN n i), rtac (isNode_def RS ssubst),
               rtac exI, rtac conjI,
               (if n = 1 then rtac @{thm if_P} THEN' etac length_Lev'
               else rtac (@{thm if_P} RS arg_cong RS trans) THEN' etac length_Lev' THEN'
                 etac (sum_case_weak_cong RS trans) THEN' rtac (mk_sum_casesN n i)),
-              EVERY' (map2 (fn set_map => fn set_rv_Lev =>
-                EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map RS trans),
+              EVERY' (map2 (fn set_map0 => fn set_rv_Lev =>
+                EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map0 RS trans),
                   rtac trans_fun_cong_image_id_id_apply,
                   etac set_rv_Lev, TRY o atac, etac conjI, atac])
-              (take m set_maps) set_rv_Levs),
-              CONJ_WRAP' (fn (set_map, (set_Lev, set_image_Lev)) =>
-                EVERY' [rtac (set_map RS trans), rtac equalityI, rtac @{thm image_subsetI},
+              (take m set_map0s) set_rv_Levs),
+              CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) =>
+                EVERY' [rtac (set_map0 RS trans), rtac equalityI, rtac @{thm image_subsetI},
                   rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, etac set_Lev,
                   if n = 1 then rtac refl else atac, atac, rtac subsetI,
                   REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
                   rtac set_image_Lev, atac, dtac length_Lev, hyp_subst_tac ctxt, dtac length_Lev',
                   etac @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]},
                   if n = 1 then rtac refl else atac])
-              (drop m set_maps ~~ (set_Levs ~~ set_image_Levs))])
-          ks isNode_defs set_mapss set_rv_Levss set_Levss set_image_Levss),
-          CONJ_WRAP' (fn (i, (rv_last, (isNode_def, (set_maps,
+              (drop m set_map0s ~~ (set_Levs ~~ set_image_Levs))])
+          ks isNode_defs set_map0ss set_rv_Levss set_Levss set_image_Levss),
+          CONJ_WRAP' (fn (i, (rv_last, (isNode_def, (set_map0s,
             (set_rv_Levs, (set_Levs, set_image_Levs)))))) =>
             EVERY' [rtac ballI,
               REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
@@ -739,13 +739,13 @@
               (if n = 1 then rtac @{thm if_P} THEN' etac length_Lev'
               else rtac (@{thm if_P} RS trans) THEN' etac length_Lev' THEN'
                 etac (sum_case_weak_cong RS trans) THEN' rtac (mk_sum_casesN n i)),
-              EVERY' (map2 (fn set_map => fn set_rv_Lev =>
-                EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map RS trans),
+              EVERY' (map2 (fn set_map0 => fn set_rv_Lev =>
+                EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map0 RS trans),
                   rtac trans_fun_cong_image_id_id_apply,
                   etac set_rv_Lev, TRY o atac, etac conjI, atac])
-              (take m set_maps) set_rv_Levs),
-              CONJ_WRAP' (fn (set_map, (set_Lev, set_image_Lev)) =>
-                EVERY' [rtac (set_map RS trans), rtac equalityI, rtac @{thm image_subsetI},
+              (take m set_map0s) set_rv_Levs),
+              CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) =>
+                EVERY' [rtac (set_map0 RS trans), rtac equalityI, rtac @{thm image_subsetI},
                   rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, etac set_Lev,
                   if n = 1 then rtac refl else atac, atac, rtac subsetI,
                   REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
@@ -754,8 +754,8 @@
                   atac, dtac length_Lev, hyp_subst_tac ctxt, dtac length_Lev',
                   etac @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]},
                   if n = 1 then rtac refl else atac])
-              (drop m set_maps ~~ (set_Levs ~~ set_image_Levs))])
-          (ks ~~ (rv_lasts ~~ (isNode_defs ~~ (set_mapss ~~
+              (drop m set_map0s ~~ (set_Levs ~~ set_image_Levs))])
+          (ks ~~ (rv_lasts ~~ (isNode_defs ~~ (set_map0ss ~~
             (set_rv_Levss ~~ (set_Levss ~~ set_image_Levss)))))),
         (**)
           rtac allI, rtac impI, rtac @{thm if_not_P}, rtac notI,
@@ -766,12 +766,12 @@
           CONVERSION (Conv.top_conv
             (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
           if n = 1 then rtac refl else rtac (mk_sum_casesN n i),
-          EVERY' (map2 (fn set_map => fn coalg_set =>
-            EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map RS trans),
+          EVERY' (map2 (fn set_map0 => fn coalg_set =>
+            EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map0 RS trans),
               rtac trans_fun_cong_image_id_id_apply, etac coalg_set, atac])
-            (take m set_maps) (take m coalg_sets)),
-          CONJ_WRAP' (fn (set_map, (set_Lev, set_image_Lev)) =>
-            EVERY' [rtac (set_map RS trans), rtac equalityI, rtac @{thm image_subsetI},
+            (take m set_map0s) (take m coalg_sets)),
+          CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) =>
+            EVERY' [rtac (set_map0 RS trans), rtac equalityI, rtac @{thm image_subsetI},
               rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, rtac set_Lev,
               rtac (Lev_0 RS equalityD2 RS set_mp), rtac @{thm singletonI}, rtac rv_Nil,
               atac, rtac subsetI,
@@ -781,7 +781,7 @@
               etac @{thm set_mp[OF equalityD1[OF arg_cong[OF
                 trans[OF length_append_singleton arg_cong[of _ _ Suc, OF list.size(3)]]]]]},
               rtac rv_Nil])
-          (drop m set_maps ~~ (nth set_Levss (i - 1) ~~ nth set_image_Levss (i - 1)))];
+          (drop m set_map0s ~~ (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_cong0, map_arg_cong)), (length_Lev', (from_to_sbds, to_sbd_injs)))))) =
@@ -842,7 +842,7 @@
     CONJ_WRAP' fbetw_tac
       (ks ~~ (carT_defs ~~ (isNode_defs ~~ (Lev_0s ~~ (rv_Nils ~~ (Lev_sbds ~~
         ((length_Levs ~~ length_Lev's) ~~ (prefCl_Levs ~~ (rv_lastss ~~
-          (set_mapss ~~ (coalg_setss ~~
+          (set_map0ss ~~ (coalg_setss ~~
             (set_rv_Levsss ~~ (set_Levsss ~~ set_image_Levsss))))))))))))) THEN'
     CONJ_WRAP' mor_tac
       (ks ~~ (strT_defs ~~ (((Lev_0s ~~ Lev_Sucs) ~~ (rv_Nils ~~ rv_Conss)) ~~
@@ -860,22 +860,22 @@
     equiv_LSBISs), rtac sym, rtac (o_apply RS trans),
     etac (sym RS arg_cong RS trans), rtac map_comp_id] 1;
 
-fun mk_coalg_final_tac m coalg_def congruent_str_finals equiv_LSBISs set_mapss coalgT_setss =
+fun mk_coalg_final_tac m coalg_def congruent_str_finals equiv_LSBISs set_map0ss coalgT_setss =
   EVERY' [stac coalg_def,
-    CONJ_WRAP' (fn ((set_maps, coalgT_sets), (equiv_LSBIS, congruent_str_final)) =>
+    CONJ_WRAP' (fn ((set_map0s, coalgT_sets), (equiv_LSBIS, congruent_str_final)) =>
       EVERY' [rtac @{thm univ_preserves}, rtac equiv_LSBIS, rtac congruent_str_final,
         rtac ballI, rtac @{thm ssubst_mem}, rtac o_apply, rtac CollectI,
-        EVERY' (map2 (fn set_map => fn coalgT_set =>
-          EVERY' [rtac conjI, rtac (set_map RS ord_eq_le_trans),
+        EVERY' (map2 (fn set_map0 => fn coalgT_set =>
+          EVERY' [rtac conjI, rtac (set_map0 RS ord_eq_le_trans),
             rtac ord_eq_le_trans_trans_fun_cong_image_id_id_apply,
             etac coalgT_set])
-        (take m set_maps) (take m coalgT_sets)),
-        CONJ_WRAP' (fn (equiv_LSBIS, (set_map, coalgT_set)) =>
-          EVERY' [rtac (set_map RS ord_eq_le_trans),
+        (take m set_map0s) (take m coalgT_sets)),
+        CONJ_WRAP' (fn (equiv_LSBIS, (set_map0, coalgT_set)) =>
+          EVERY' [rtac (set_map0 RS ord_eq_le_trans),
             rtac @{thm image_subsetI}, rtac ssubst, rtac @{thm proj_in_iff},
             rtac equiv_LSBIS, etac set_rev_mp, etac coalgT_set])
-        (equiv_LSBISs ~~ drop m (set_maps ~~ coalgT_sets))])
-    ((set_mapss ~~ coalgT_setss) ~~ (equiv_LSBISs ~~ congruent_str_finals))] 1;
+        (equiv_LSBISs ~~ drop m (set_map0s ~~ coalgT_sets))])
+    ((set_map0ss ~~ coalgT_setss) ~~ (equiv_LSBISs ~~ congruent_str_finals))] 1;
 
 fun mk_mor_T_final_tac mor_def congruent_str_finals equiv_LSBISs =
   EVERY' [stac mor_def, rtac conjI,
@@ -1049,7 +1049,7 @@
         replicate n (@{thm o_id} RS fun_cong))))
     maps map_comp0s map_cong0s)] 1;
 
-fun mk_mcong_tac ctxt m coinduct_tac map_comps dtor_maps map_cong0s set_mapss set_hsetss
+fun mk_mcong_tac ctxt m coinduct_tac map_comps dtor_maps map_cong0s set_map0ss set_hsetss
   set_hset_hsetsss =
   let
     val n = length map_comps;
@@ -1057,7 +1057,7 @@
   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_map0s), 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,
@@ -1068,16 +1068,16 @@
            [rtac o_apply_trans_sym, rtac (id_apply RS trans), etac CollectE,
            REPEAT_DETERM o etac conjE, etac bspec, etac set_hset]) set_hsets),
          REPEAT_DETERM_N n o rtac snd_convol_fun_cong_sym,
-         CONJ_WRAP' (fn (set_map, set_hset_hsets) =>
+         CONJ_WRAP' (fn (set_map0, set_hset_hsets) =>
            EVERY' [REPEAT_DETERM o rtac allI, rtac impI, rtac @{thm image_convolD},
-             etac set_rev_mp, rtac ord_eq_le_trans, rtac set_map,
+             etac set_rev_mp, rtac ord_eq_le_trans, rtac set_map0,
              rtac @{thm image_mono}, rtac subsetI, rtac CollectI, etac CollectE,
              REPEAT_DETERM o etac conjE,
              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)])
+           (drop m set_map0s ~~ set_hset_hsetss)])
         (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) @
+          map_cong0s ~~ set_map0ss ~~ 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,
@@ -1089,7 +1089,7 @@
   unfold_thms_tac ctxt (sym_map_comps @ @{thms o_assoc id_o o_id}) THEN
   ALLGOALS (etac sym);
 
-fun mk_col_natural_tac cts rec_0s rec_Sucs dtor_maps set_mapss
+fun mk_col_natural_tac cts rec_0s rec_Sucs dtor_maps set_map0ss
   {context = ctxt, prems = _} =
   let
     val n = length dtor_maps;
@@ -1105,10 +1105,10 @@
         CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 Un_cong))
           (fn i => EVERY' [rtac @{thm UN_cong[OF refl]},
             REPEAT_DETERM o etac allE, etac (mk_conjunctN n i)]) (n downto 1)])
-      (rec_Sucs ~~ (dtor_maps ~~ set_mapss))] 1
+      (rec_Sucs ~~ (dtor_maps ~~ set_map0ss))] 1
   end;
 
-fun mk_set_map_tac hset_def col_natural =
+fun mk_set_map0_tac hset_def col_natural =
   EVERY' (map rtac [ext, (o_apply RS trans), (hset_def RS trans), sym,
     (o_apply RS trans), (@{thm image_cong} OF [hset_def, refl] RS trans),
     (@{thm image_UN} RS trans), (refl RS @{thm UN_cong}), col_natural]) 1;
@@ -1158,10 +1158,10 @@
       REPEAT_DETERM o eresolve_tac [CollectE, conjE], etac map_eq]
   end;
 
-fun mk_coalg_thePull_tac m coalg_def map_wpulls set_mapss pickWP_assms_tacs
+fun mk_coalg_thePull_tac m coalg_def map_wpulls set_map0ss pickWP_assms_tacs
   {context = ctxt, prems = _} =
   unfold_thms_tac ctxt [coalg_def] THEN
-  CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, set_maps)) =>
+  CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, set_map0s)) =>
     EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
       REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}],
       hyp_subst_tac ctxt, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}),
@@ -1171,11 +1171,11 @@
       REPEAT_DETERM o eresolve_tac [CollectE, conjE],
       rtac CollectI,
       REPEAT_DETERM_N m o (rtac conjI THEN' rtac subset_UNIV),
-      CONJ_WRAP' (fn set_map =>
-        EVERY' [rtac ord_eq_le_trans, rtac trans, rtac set_map,
+      CONJ_WRAP' (fn set_map0 =>
+        EVERY' [rtac ord_eq_le_trans, rtac trans, rtac set_map0,
           rtac trans_fun_cong_image_id_id_apply, atac])
-      (drop m set_maps)])
-  (map_wpulls ~~ (pickWP_assms_tacs ~~ set_mapss)) 1;
+      (drop m set_map0s)])
+  (map_wpulls ~~ (pickWP_assms_tacs ~~ set_map0ss)) 1;
 
 fun mk_mor_thePull_nth_tac conv pick m mor_def map_wpulls map_comp0s pickWP_assms_tacs
   {context = ctxt, prems = _: thm list} =
@@ -1210,7 +1210,7 @@
       rtac refl])
   (unfolds ~~ map_comp0s) 1;
 
-fun mk_pick_col_tac m j cts rec_0s rec_Sucs unfolds set_mapss map_wpulls pickWP_assms_tacs
+fun mk_pick_col_tac m j cts rec_0s rec_Sucs unfolds set_map0ss map_wpulls pickWP_assms_tacs
   {context = ctxt, prems = _} =
   let
     val n = length rec_0s;
@@ -1221,7 +1221,7 @@
       CONJ_WRAP' (fn thm => EVERY'
         [rtac impI, rtac ord_eq_le_trans, rtac thm, rtac @{thm empty_subsetI}]) rec_0s,
       REPEAT_DETERM o rtac allI,
-      CONJ_WRAP' (fn (rec_Suc, ((unfold, set_maps), (map_wpull, pickWP_assms_tac))) =>
+      CONJ_WRAP' (fn (rec_Suc, ((unfold, set_map0s), (map_wpull, pickWP_assms_tac))) =>
         EVERY' [rtac impI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
           REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}],
           hyp_subst_tac ctxt, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}),
@@ -1230,16 +1230,16 @@
           rtac impI, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
           rtac ord_eq_le_trans, rtac rec_Suc,
           rtac @{thm Un_least},
-          SELECT_GOAL (unfold_thms_tac ctxt [unfold, nth set_maps (j - 1),
+          SELECT_GOAL (unfold_thms_tac ctxt [unfold, nth set_map0s (j - 1),
             @{thm prod.cases}]),
           etac ord_eq_le_trans_trans_fun_cong_image_id_id_apply,
-          CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least})) (fn (i, set_map) =>
+          CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least})) (fn (i, set_map0) =>
             EVERY' [rtac @{thm UN_least},
-              SELECT_GOAL (unfold_thms_tac ctxt [unfold, set_map, @{thm prod.cases}]),
+              SELECT_GOAL (unfold_thms_tac ctxt [unfold, set_map0, @{thm prod.cases}]),
               etac imageE, hyp_subst_tac ctxt, REPEAT_DETERM o etac allE,
               dtac (mk_conjunctN n i), etac mp, etac set_mp, atac])
-          (ks ~~ rev (drop m set_maps))])
-      (rec_Sucs ~~ ((unfolds ~~ set_mapss) ~~ (map_wpulls ~~ pickWP_assms_tacs)))] 1
+          (ks ~~ rev (drop m set_map0s))])
+      (rec_Sucs ~~ ((unfolds ~~ set_map0ss) ~~ (map_wpulls ~~ pickWP_assms_tacs)))] 1
   end;
 
 fun mk_wpull_tac m coalg_thePull mor_thePull_fst mor_thePull_snd mor_thePull_pick
@@ -1288,26 +1288,26 @@
     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_comp0 map_cong0 dtor_map dtor_sets dtor_inject
-    dtor_ctor set_maps dtor_set_incls dtor_set_set_inclss =
+    dtor_ctor set_map0s dtor_set_incls dtor_set_set_inclss =
   let
     val m = length dtor_set_incls;
     val n = length dtor_set_set_inclss;
-    val (passive_set_maps, active_set_maps) = chop m set_maps;
+    val (passive_set_map0s, active_set_map0s) = chop m set_map0s;
     val in_Jrel = nth in_Jrels (i - 1);
     val if_tac =
       EVERY' [dtac (in_Jrel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
         rtac (in_rel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
-        EVERY' (map2 (fn set_map => fn set_incl =>
-          EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_map,
+        EVERY' (map2 (fn set_map0 => fn set_incl =>
+          EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_map0,
             rtac ord_eq_le_trans, rtac trans_fun_cong_image_id_id_apply,
             etac (set_incl RS @{thm subset_trans})])
-        passive_set_maps dtor_set_incls),
-        CONJ_WRAP' (fn (in_Jrel, (set_map, dtor_set_set_incls)) =>
-          EVERY' [rtac ord_eq_le_trans, rtac set_map, rtac @{thm image_subsetI}, rtac CollectI,
+        passive_set_map0s dtor_set_incls),
+        CONJ_WRAP' (fn (in_Jrel, (set_map0, dtor_set_set_incls)) =>
+          EVERY' [rtac ord_eq_le_trans, rtac set_map0, rtac @{thm image_subsetI}, rtac CollectI,
             rtac @{thm prod_caseI}, rtac (in_Jrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
             CONJ_WRAP' (fn thm => etac (thm RS @{thm subset_trans}) THEN' atac) dtor_set_set_incls,
             rtac conjI, rtac refl, rtac refl])
-        (in_Jrels ~~ (active_set_maps ~~ dtor_set_set_inclss)),
+        (in_Jrels ~~ (active_set_map0s ~~ dtor_set_set_inclss)),
         CONJ_WRAP' (fn conv =>
           EVERY' [rtac trans, rtac map_comp0, rtac trans, rtac map_cong0,
           REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
@@ -1317,14 +1317,14 @@
     val only_if_tac =
       EVERY' [dtac (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
         rtac (in_Jrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
-        CONJ_WRAP' (fn (dtor_set, passive_set_map) =>
+        CONJ_WRAP' (fn (dtor_set, passive_set_map0) =>
           EVERY' [rtac ord_eq_le_trans, rtac dtor_set, rtac @{thm Un_least},
-            rtac ord_eq_le_trans, rtac box_equals, rtac passive_set_map,
+            rtac ord_eq_le_trans, rtac box_equals, rtac passive_set_map0,
             rtac (dtor_ctor RS sym RS arg_cong), rtac trans_fun_cong_image_id_id_apply, atac,
             CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
-              (fn (active_set_map, in_Jrel) => EVERY' [rtac ord_eq_le_trans,
+              (fn (active_set_map0, in_Jrel) => EVERY' [rtac ord_eq_le_trans,
                 rtac @{thm UN_cong[OF _ refl]}, rtac @{thm box_equals[OF _ _ refl]},
-                rtac active_set_map, rtac (dtor_ctor RS sym RS arg_cong), rtac @{thm UN_least},
+                rtac active_set_map0, rtac (dtor_ctor RS sym RS arg_cong), rtac @{thm UN_least},
                 dtac set_rev_mp, etac @{thm image_mono}, etac imageE,
                 dtac @{thm ssubst_mem[OF pair_collapse]},
                 REPEAT_DETERM o eresolve_tac (CollectE :: conjE ::
@@ -1335,8 +1335,8 @@
                 TRY o
                   EVERY' [dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac, hyp_subst_tac ctxt],
                 REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
-            (rev (active_set_maps ~~ in_Jrels))])
-        (dtor_sets ~~ passive_set_maps),
+            (rev (active_set_map0s ~~ in_Jrels))])
+        (dtor_sets ~~ passive_set_map0s),
         rtac conjI,
         REPEAT_DETERM_N 2 o EVERY'[rtac (dtor_inject RS iffD1), rtac trans, rtac dtor_map,
           rtac box_equals, rtac map_comp0, rtac (dtor_ctor RS sym RS arg_cong), rtac trans,
@@ -1352,12 +1352,12 @@
     EVERY' [rtac iffI, if_tac, only_if_tac] 1
   end;
 
-fun mk_rel_coinduct_coind_tac m coinduct ks map_comp0s map_congs map_arg_congs set_mapss 
+fun mk_rel_coinduct_coind_tac m coinduct ks map_comp0s map_congs map_arg_congs set_map0ss 
   dtor_unfolds dtor_maps {context = ctxt, prems = _} =
   let val n = length ks;
   in
     EVERY' [DETERM o rtac coinduct,
-      EVERY' (map7 (fn i => fn map_comp0 => 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_map0s =>
           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,
@@ -1372,41 +1372,41 @@
           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),
           SELECT_GOAL (unfold_thms_tac ctxt @{thms prod.cases}), 
-          CONJ_WRAP' (fn set_map =>
+          CONJ_WRAP' (fn set_map0 =>
             EVERY' [REPEAT_DETERM o resolve_tac [allI, impI],
-              dtac (set_map RS equalityD1 RS set_mp),
+              dtac (set_map0 RS equalityD1 RS set_mp),
               REPEAT_DETERM o
                 eresolve_tac (imageE :: conjE :: @{thms iffD1[OF Pair_eq, elim_format]}),
               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_comp0s map_congs map_arg_congs set_mapss dtor_unfolds dtor_maps)] 1
+          (drop m set_map0s)])
+      ks map_comp0s map_congs map_arg_congs set_map0ss dtor_unfolds dtor_maps)] 1
   end;
 
 val split_id_unfolds = @{thms prod.cases image_id id_apply};
 
-fun mk_rel_coinduct_ind_tac m ks unfolds set_mapss j set_induct {context = ctxt, prems = _} =
+fun mk_rel_coinduct_ind_tac m ks unfolds set_map0ss j set_induct {context = ctxt, prems = _} =
   let val n = length ks;
   in
     rtac set_induct 1 THEN
-    EVERY' (map3 (fn unfold => fn set_maps => fn i =>
+    EVERY' (map3 (fn unfold => fn set_map0s => fn i =>
       EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], etac conjE,
         select_prem_tac n (dtac @{thm spec2}) i, dtac mp, atac,
         REPEAT_DETERM o eresolve_tac [CollectE, conjE, Collect_splitD_set_mp, set_rev_mp],
         hyp_subst_tac ctxt,
-        SELECT_GOAL (unfold_thms_tac ctxt ([unfold, nth set_maps (j - 1)] @ split_id_unfolds)),
+        SELECT_GOAL (unfold_thms_tac ctxt ([unfold, nth set_map0s (j - 1)] @ split_id_unfolds)),
         rtac subset_refl])
-    unfolds set_mapss ks) 1 THEN
-    EVERY' (map3 (fn unfold => fn set_maps => fn i =>
-      EVERY' (map (fn set_map =>
+    unfolds set_map0ss ks) 1 THEN
+    EVERY' (map3 (fn unfold => fn set_map0s => fn i =>
+      EVERY' (map (fn set_map0 =>
         EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], etac conjE,
         select_prem_tac n (dtac @{thm spec2}) i, dtac mp, atac,
         REPEAT_DETERM o eresolve_tac [CollectE, conjE], hyp_subst_tac ctxt,
-        SELECT_GOAL (unfold_thms_tac ctxt ([unfold, set_map] @ split_id_unfolds)),
+        SELECT_GOAL (unfold_thms_tac ctxt ([unfold, set_map0] @ split_id_unfolds)),
         etac imageE, hyp_subst_tac ctxt, REPEAT_DETERM o eresolve_tac [allE, mp],
         rtac conjI, etac Collect_splitD_set_mp, atac, rtac (@{thm surjective_pairing} RS arg_cong)])
-      (drop m set_maps)))
-    unfolds set_mapss ks) 1
+      (drop m set_map0s)))
+    unfolds set_map0ss ks) 1
   end;
 
 fun mk_rel_coinduct_tac in_rels in_Jrels helper_indss helper_coind1s helper_coind2s

--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Thu Aug 29 22:39:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Thu Aug 29 22:56:39 2013 +0200
@@ -1557,13 +1557,13 @@
           map (map (Term.subst_atomic_types (passiveAs ~~ passiveBs))) setss_by_bnf;
         val setss_by_range' = transpose setss_by_bnf';
 
-        val set_map_thmss =
+        val set_map0_thmss =
           let
-            fun mk_set_map f map z set set' =
+            fun mk_set_map0 f map z set set' =
               HOLogic.mk_eq (mk_image f $ (set $ z), set' $ (map $ z));
 
             fun mk_cphi f map z set set' = certify lthy
-              (Term.absfree (dest_Free z) (mk_set_map f map z set set'));
+              (Term.absfree (dest_Free z) (mk_set_map0 f map z set set'));
 
             val csetss = map (map (certify lthy)) setss_by_range';
 
@@ -1576,7 +1576,7 @@
             val goals =
               map3 (fn f => fn sets => fn sets' =>
                 HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
-                  (map4 (mk_set_map f) fs_maps Izs sets sets')))
+                  (map4 (mk_set_map0 f) fs_maps Izs sets sets')))
                   fs setss_by_range setss_by_range';
 
             fun mk_tac induct = mk_set_nat_tac m (rtac induct) set_map'ss ctor_map_thms;
@@ -1695,7 +1695,7 @@
         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 set_nat_tacss = map (map (K o mk_set_map0_tac)) (transpose set_map0_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));
         val set_bd_tacss = map (map (fn thm => K (rtac thm 1))) (transpose set_bd_thmss);
@@ -1775,10 +1775,10 @@
           in
             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 =>
+              fn set_map0s => 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_comp0 map_cong0 ctor_map ctor_sets
-                 ctor_inject ctor_dtor set_maps ctor_set_incls ctor_set_set_inclss))
+                 ctor_inject ctor_dtor set_map0s ctor_set_incls ctor_set_set_inclss))
               |> Thm.close_derivation)
             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

--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Thu Aug 29 22:39:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Thu Aug 29 22:56:39 2013 +0200
@@ -72,7 +72,7 @@
     {prems: 'a, context: Proof.context} -> tactic
   val mk_set_nat_tac: int -> (int -> tactic) -> thm list list -> thm list -> cterm list ->
     thm list -> int -> {prems: 'a, context: Proof.context} -> tactic
-  val mk_set_map_tac: thm -> tactic
+  val mk_set_map0_tac: thm -> tactic
   val mk_set_tac: thm -> tactic
   val mk_wit_tac: Proof.context -> int -> thm list -> thm list -> tactic
   val mk_wpull_tac: thm -> tactic
@@ -724,7 +724,7 @@
     (rtac sym THEN' rtac unique' THEN' EVERY' (map2 mk_comp map_comp0s' ctor_maps')) 1
   end;
 
-fun mk_set_map_tac set_nat =
+fun mk_set_map0_tac set_nat =
   EVERY' (map rtac [ext, trans, o_apply, sym, trans, o_apply, set_nat]) 1;
 
 fun mk_bd_card_order_tac bd_card_orders =
@@ -747,31 +747,31 @@
             REPEAT_DETERM_N n o etac UnE]))))] 1);
 
 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 =
+  ctor_dtor set_map0s ctor_set_incls ctor_set_set_inclss =
   let
     val m = length ctor_set_incls;
     val n = length ctor_set_set_inclss;
 
-    val (passive_set_maps, active_set_maps) = chop m set_maps;
+    val (passive_set_map0s, active_set_map0s) = chop m set_map0s;
     val in_Irel = nth in_Irels (i - 1);
     val le_arg_cong_ctor_dtor = ctor_dtor RS arg_cong RS ord_eq_le_trans;
     val eq_arg_cong_ctor_dtor = ctor_dtor RS arg_cong RS trans;
     val if_tac =
       EVERY' [dtac (in_Irel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
         rtac (in_rel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
-        EVERY' (map2 (fn set_map => fn ctor_set_incl =>
-          EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_map,
+        EVERY' (map2 (fn set_map0 => fn ctor_set_incl =>
+          EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_map0,
             rtac ord_eq_le_trans, rtac trans_fun_cong_image_id_id_apply,
             rtac (ctor_set_incl RS subset_trans), etac le_arg_cong_ctor_dtor])
-        passive_set_maps ctor_set_incls),
-        CONJ_WRAP' (fn (in_Irel, (set_map, ctor_set_set_incls)) =>
-          EVERY' [rtac ord_eq_le_trans, rtac set_map, rtac @{thm image_subsetI}, rtac CollectI,
+        passive_set_map0s ctor_set_incls),
+        CONJ_WRAP' (fn (in_Irel, (set_map0, ctor_set_set_incls)) =>
+          EVERY' [rtac ord_eq_le_trans, rtac set_map0, rtac @{thm image_subsetI}, rtac CollectI,
             rtac @{thm prod_caseI}, rtac (in_Irel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
             CONJ_WRAP' (fn thm =>
               EVERY' (map etac [thm RS subset_trans, le_arg_cong_ctor_dtor]))
             ctor_set_set_incls,
             rtac conjI, rtac refl, rtac refl])
-        (in_Irels ~~ (active_set_maps ~~ ctor_set_set_inclss)),
+        (in_Irels ~~ (active_set_map0s ~~ ctor_set_set_inclss)),
         CONJ_WRAP' (fn conv =>
           EVERY' [rtac trans, rtac map_comp0, rtac trans, rtac map_cong0,
           REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
@@ -782,13 +782,13 @@
     val only_if_tac =
       EVERY' [dtac (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
         rtac (in_Irel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
-        CONJ_WRAP' (fn (ctor_set, passive_set_map) =>
+        CONJ_WRAP' (fn (ctor_set, passive_set_map0) =>
           EVERY' [rtac ord_eq_le_trans, rtac ctor_set, rtac @{thm Un_least},
             rtac ord_eq_le_trans, rtac @{thm box_equals[OF _ refl]},
-            rtac passive_set_map, rtac trans_fun_cong_image_id_id_apply, atac,
+            rtac passive_set_map0, rtac trans_fun_cong_image_id_id_apply, atac,
             CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
-              (fn (active_set_map, in_Irel) => EVERY' [rtac ord_eq_le_trans,
-                rtac @{thm UN_cong[OF _ refl]}, rtac active_set_map, rtac @{thm UN_least},
+              (fn (active_set_map0, in_Irel) => EVERY' [rtac ord_eq_le_trans,
+                rtac @{thm UN_cong[OF _ refl]}, rtac active_set_map0, rtac @{thm UN_least},
                 dtac set_rev_mp, etac @{thm image_mono}, etac imageE,
                 dtac @{thm ssubst_mem[OF pair_collapse]},
                 REPEAT_DETERM o eresolve_tac (CollectE :: conjE ::
@@ -798,8 +798,8 @@
                 TRY o
                   EVERY' [dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac, hyp_subst_tac ctxt],
                 REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
-            (rev (active_set_maps ~~ in_Irels))])
-        (ctor_sets ~~ passive_set_maps),
+            (rev (active_set_map0s ~~ in_Irels))])
+        (ctor_sets ~~ passive_set_map0s),
         rtac conjI,
         REPEAT_DETERM_N 2 o EVERY' [rtac trans, rtac ctor_map, rtac (ctor_inject RS iffD2),
           rtac trans, rtac map_comp0, rtac trans, rtac map_cong0,