tuned a few ML names

--- a/src/HOL/Codatatype/Tools/bnf_comp.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp.ML	Fri Sep 21 15:53:29 2012 +0200
@@ -8,21 +8,21 @@
 
 signature BNF_COMP =
 sig
-  type unfold_thms
-  val empty_unfold: unfold_thms
-  val map_unfolds_of: unfold_thms -> thm list
-  val set_unfoldss_of: unfold_thms -> thm list list
-  val pred_unfolds_of: unfold_thms -> thm list
-  val rel_unfolds_of: unfold_thms -> thm list
+  type unfold_set
+  val empty_unfolds: unfold_set
+  val map_unfolds_of: unfold_set -> thm list
+  val set_unfoldss_of: unfold_set -> thm list list
+  val pred_unfolds_of: unfold_set -> thm list
+  val rel_unfolds_of: unfold_set -> thm list
 
   val bnf_of_typ: BNF_Def.const_policy -> (binding -> binding) ->
-    ((string * sort) list list -> (string * sort) list) -> typ -> unfold_thms * Proof.context ->
-    (BNF_Def.BNF * (typ list * typ list)) * (unfold_thms * Proof.context)
+    ((string * sort) list list -> (string * sort) list) -> typ -> unfold_set * Proof.context ->
+    (BNF_Def.BNF * (typ list * typ list)) * (unfold_set * Proof.context)
   val default_comp_sort: (string * sort) list list -> (string * sort) list
   val normalize_bnfs: (int -> binding -> binding) -> ''a list list -> ''a list ->
-    (''a list list -> ''a list) -> BNF_Def.BNF list -> unfold_thms -> Proof.context ->
-    (int list list * ''a list) * (BNF_Def.BNF list * (unfold_thms * Proof.context))
-  val seal_bnf: unfold_thms -> binding -> typ list -> BNF_Def.BNF -> Proof.context ->
+    (''a list list -> ''a list) -> BNF_Def.BNF list -> unfold_set -> Proof.context ->
+    (int list list * ''a list) * (BNF_Def.BNF list * (unfold_set * Proof.context))
+  val seal_bnf: unfold_set -> binding -> typ list -> BNF_Def.BNF -> Proof.context ->
     (BNF_Def.BNF * typ list) * local_theory
 end;
 
@@ -34,7 +34,7 @@
 open BNF_Tactics
 open BNF_Comp_Tactics
 
-type unfold_thms = {
+type unfold_set = {
   map_unfolds: thm list,
   set_unfoldss: thm list list,
   pred_unfolds: thm list,
@@ -46,17 +46,17 @@
 fun adds_to_thms thms NONE = thms
   | adds_to_thms thms (SOME news) = insert (eq_set Thm.eq_thm) (no_reflexive news) thms;
 
-val empty_unfold = {map_unfolds = [], set_unfoldss = [], pred_unfolds = [], rel_unfolds = []};
+val empty_unfolds = {map_unfolds = [], set_unfoldss = [], pred_unfolds = [], rel_unfolds = []};
 
-fun add_to_unfold_opt map_opt sets_opt pred_opt rel_opt
+fun add_to_unfolds_opt map_opt sets_opt pred_opt rel_opt
   {map_unfolds, set_unfoldss, pred_unfolds, rel_unfolds} =
   {map_unfolds = add_to_thms map_unfolds map_opt,
     set_unfoldss = adds_to_thms set_unfoldss sets_opt,
     pred_unfolds = add_to_thms pred_unfolds pred_opt,
     rel_unfolds = add_to_thms rel_unfolds rel_opt};
 
-fun add_to_unfold map sets pred rel =
-  add_to_unfold_opt (SOME map) (SOME sets) (SOME pred) (SOME rel);
+fun add_to_unfolds map sets pred rel =
+  add_to_unfolds_opt (SOME map) (SOME sets) (SOME pred) (SOME rel);
 
 val map_unfolds_of = #map_unfolds;
 val set_unfoldss_of = #set_unfoldss;
@@ -77,7 +77,7 @@
     val get = fn Const (x, _) => AList.lookup (op =) eqs x | _ => NONE;
   in Envir.expand_term get end;
 
-fun clean_compose_bnf const_policy qualify b outer inners (unfold, lthy) =
+fun clean_compose_bnf const_policy qualify b outer inners (unfold_set, lthy) =
   let
     val olive = live_of_bnf outer;
     val onwits = nwits_of_bnf outer;
@@ -274,15 +274,16 @@
       bnf_def const_policy (K Derive_Few_Facts) qualify tacs wit_tac (SOME (oDs @ flat Dss))
         (((((b, mapx), sets), bd), wits), SOME pred) lthy;
 
-    val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (pred_def_of_bnf bnf')
-      (rel_def_of_bnf bnf') unfold;
+    val unfold_set' =
+      add_to_unfolds (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (pred_def_of_bnf bnf')
+        (rel_def_of_bnf bnf') unfold_set;
   in
-    (bnf', (unfold', lthy'))
+    (bnf', (unfold_set', lthy'))
   end;
 
 (* Killing live variables *)
 
-fun kill_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else
+fun kill_bnf qualify n bnf (unfold_set, lthy) = if n = 0 then (bnf, (unfold_set, lthy)) else
   let
     val b = Binding.suffix_name (mk_killN n) (name_of_bnf bnf);
     val live = live_of_bnf bnf;
@@ -375,15 +376,16 @@
       bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME (killedAs @ Ds))
         (((((b, mapx), sets), Term.absdummy T bd), wits), SOME pred) lthy;
 
-    val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (pred_def_of_bnf bnf')
-      (rel_def_of_bnf bnf') unfold;
+    val unfold_set' =
+      add_to_unfolds (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (pred_def_of_bnf bnf')
+        (rel_def_of_bnf bnf') unfold_set;
   in
-    (bnf', (unfold', lthy'))
+    (bnf', (unfold_set', lthy'))
   end;
 
 (* Adding dummy live variables *)
 
-fun lift_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else
+fun lift_bnf qualify n bnf (unfold_set, lthy) = if n = 0 then (bnf, (unfold_set, lthy)) else
   let
     val b = Binding.suffix_name (mk_liftN n) (name_of_bnf bnf);
     val live = live_of_bnf bnf;
@@ -462,15 +464,17 @@
       bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME Ds)
         (((((b, mapx), sets), Term.absdummy T bd), wits), SOME pred) lthy;
 
-    val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (pred_def_of_bnf bnf')
-      (pred_def_of_bnf bnf') unfold;
+    val unfold_set' =
+      add_to_unfolds (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (pred_def_of_bnf bnf')
+        (pred_def_of_bnf bnf') unfold_set;
   in
-    (bnf', (unfold', lthy'))
+    (bnf', (unfold_set', lthy'))
   end;
 
 (* Changing the order of live variables *)
 
-fun permute_bnf qualify src dest bnf (unfold, lthy) = if src = dest then (bnf, (unfold, lthy)) else
+fun permute_bnf qualify src dest bnf (unfold_set, lthy) =
+  if src = dest then (bnf, (unfold_set, lthy)) else
   let
     val b = Binding.suffix_name (mk_permuteN src dest) (name_of_bnf bnf);
     val live = live_of_bnf bnf;
@@ -540,10 +544,11 @@
       bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME Ds)
         (((((b, mapx), sets), Term.absdummy T bd), wits), SOME pred) lthy;
 
-    val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (pred_def_of_bnf bnf')
-      (pred_def_of_bnf bnf') unfold;
+    val unfold_set' =
+      add_to_unfolds (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (pred_def_of_bnf bnf')
+        (pred_def_of_bnf bnf') unfold_set;
   in
-    (bnf', (unfold', lthy'))
+    (bnf', (unfold_set', lthy'))
   end;
 
 (* Composition pipeline *)
@@ -558,17 +563,17 @@
   |> lift_bnf qualify n
   #> uncurry (permute_bnf qualify src dest);
 
-fun normalize_bnfs qualify Ass Ds sort bnfs unfold lthy =
+fun normalize_bnfs qualify Ass Ds sort bnfs unfold_set lthy =
   let
     val before_kill_src = map (fn As => 0 upto (length As - 1)) Ass;
     val kill_poss = map (find_indices Ds) Ass;
     val live_poss = map2 (subtract (op =)) kill_poss before_kill_src;
     val before_kill_dest = map2 append kill_poss live_poss;
     val kill_ns = map length kill_poss;
-    val (inners', (unfold', lthy')) =
+    val (inners', (unfold_set', lthy')) =
       fold_map5 (fn i => permute_and_kill (qualify i))
         (if length bnfs = 1 then [0] else (1 upto length bnfs))
-        kill_ns before_kill_src before_kill_dest bnfs (unfold, lthy);
+        kill_ns before_kill_src before_kill_dest bnfs (unfold_set, lthy);
 
     val Ass' = map2 (map o nth) Ass live_poss;
     val As = sort Ass';
@@ -580,32 +585,32 @@
   in
     ((kill_poss, As), fold_map5 (fn i => lift_and_permute (qualify i))
       (if length bnfs = 1 then [0] else (1 upto length bnfs))
-      lift_ns after_lift_src after_lift_dest inners' (unfold', lthy'))
+      lift_ns after_lift_src after_lift_dest inners' (unfold_set', lthy'))
   end;
 
 fun default_comp_sort Ass =
   Library.sort (Term_Ord.typ_ord o pairself TFree) (fold (fold (insert (op =))) Ass []);
 
-fun compose_bnf const_policy qualify sort outer inners oDs Dss tfreess (unfold, lthy) =
+fun compose_bnf const_policy qualify sort outer inners oDs Dss tfreess (unfold_set, lthy) =
   let
     val b = name_of_bnf outer;
 
     val Ass = map (map Term.dest_TFree) tfreess;
     val Ds = fold (fold Term.add_tfreesT) (oDs :: Dss) [];
 
-    val ((kill_poss, As), (inners', (unfold', lthy'))) =
-      normalize_bnfs qualify Ass Ds sort inners unfold lthy;
+    val ((kill_poss, As), (inners', (unfold_set', lthy'))) =
+      normalize_bnfs qualify Ass Ds sort inners unfold_set lthy;
 
     val Ds = oDs @ flat (map3 (append oo map o nth) tfreess kill_poss Dss);
     val As = map TFree As;
   in
     apfst (rpair (Ds, As))
-      (clean_compose_bnf const_policy (qualify 0) b outer inners' (unfold', lthy'))
+      (clean_compose_bnf const_policy (qualify 0) b outer inners' (unfold_set', lthy'))
   end;
 
 (* Hide the type of the bound (optimization) and unfold the definitions (nicer to the user) *)
 
-fun seal_bnf unfold b Ds bnf lthy =
+fun seal_bnf unfold_set b Ds bnf lthy =
   let
     val live = live_of_bnf bnf;
     val nwits = nwits_of_bnf bnf;
@@ -615,10 +620,10 @@
     val (Bs, _) = apfst (map TFree)
       (Variable.invent_types (replicate live HOLogic.typeS) lthy1);
 
-    val map_unfolds = map_unfolds_of unfold;
-    val set_unfoldss = set_unfoldss_of unfold;
-    val pred_unfolds = pred_unfolds_of unfold;
-    val rel_unfolds = rel_unfolds_of unfold;
+    val map_unfolds = map_unfolds_of unfold_set;
+    val set_unfoldss = set_unfoldss_of unfold_set;
+    val pred_unfolds = pred_unfolds_of unfold_set;
+    val rel_unfolds = rel_unfolds_of unfold_set;
 
     val expand_maps = fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of)
       map_unfolds);
@@ -695,13 +700,13 @@
 
 fun bnf_of_typ _ _ _ (T as TFree _) accum = ((ID_bnf, ([], [T])), accum)
   | bnf_of_typ _ _ _ (TVar _) _ = error "Unexpected schematic variable"
-  | bnf_of_typ const_policy qualify' sort (T as Type (C, Ts)) (unfold, lthy) =
+  | bnf_of_typ const_policy qualify' sort (T as Type (C, Ts)) (unfold_set, lthy) =
     let
       val tfrees = Term.add_tfreesT T [];
       val bnf_opt = if null tfrees then NONE else bnf_of lthy C;
     in
       (case bnf_opt of
-        NONE => ((DEADID_bnf, ([T], [])), (unfold, lthy))
+        NONE => ((DEADID_bnf, ([T], [])), (unfold_set, lthy))
       | SOME bnf =>
         if forall (can Term.dest_TFree) Ts andalso length Ts = length tfrees then
           let
@@ -712,7 +717,7 @@
             val deads_lives =
               pairself (map (Term.typ_subst_TVars (map fst tvars' ~~ map TFree tfrees)))
                 (deads, lives);
-          in ((bnf, deads_lives), (unfold, lthy)) end
+          in ((bnf, deads_lives), (unfold_set, lthy)) end
         else
           let
             val name = Long_Name.base_name C;
@@ -725,12 +730,12 @@
               (mk_T_of_bnf (replicate odead (TFree ("dead", []))) (replicate olive dummyT) bnf)));
             val oDs = map (nth Ts) oDs_pos;
             val Ts' = map (nth Ts) (subtract (op =) oDs_pos (0 upto length Ts - 1));
-            val ((inners, (Dss, Ass)), (unfold', lthy')) =
+            val ((inners, (Dss, Ass)), (unfold_set', lthy')) =
               apfst (apsnd split_list o split_list)
                 (fold_map2 (fn i => bnf_of_typ Smart_Inline (qualify i) sort)
-                (if length Ts' = 1 then [0] else (1 upto length Ts')) Ts' (unfold, lthy));
+                (if length Ts' = 1 then [0] else (1 upto length Ts')) Ts' (unfold_set, lthy));
           in
-            compose_bnf const_policy qualify sort bnf inners oDs Dss Ass (unfold', lthy')
+            compose_bnf const_policy qualify sort bnf inners oDs Dss Ass (unfold_set', lthy')
           end)
     end;
 

--- a/src/HOL/Codatatype/Tools/bnf_fp.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp.ML	Fri Sep 21 15:53:29 2012 +0200
@@ -375,7 +375,7 @@
   | fp_sort lhss (SOME resBs) Ass =
     (subtract (op =) lhss (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs)) @ lhss;
 
-fun mk_fp_bnf timer construct resBs bs sort lhss bnfs deadss livess unfold lthy =
+fun mk_fp_bnf timer construct resBs bs sort lhss bnfs deadss livess unfold_set lthy =
   let
     val name = mk_common_name (map Binding.name_of bs);
     fun qualify i =
@@ -392,13 +392,13 @@
 
     val timer = time (timer "Construction of BNFs");
 
-    val ((kill_poss, _), (bnfs', (unfold', lthy'))) =
-      normalize_bnfs qualify Ass Ds sort bnfs unfold lthy;
+    val ((kill_poss, _), (bnfs', (unfold_set', lthy'))) =
+      normalize_bnfs qualify Ass Ds sort bnfs unfold_set lthy;
 
     val Dss = map3 (append oo map o nth) livess kill_poss deadss;
 
     val ((bnfs'', deadss), lthy'') =
-      fold_map3 (seal_bnf unfold') (map (Binding.prefix_name preN) bs) Dss bnfs' lthy'
+      fold_map3 (seal_bnf unfold_set') (map (Binding.prefix_name preN) bs) Dss bnfs' lthy'
       |>> split_list;
 
     val timer = time (timer "Normalization & sealing of BNFs");
@@ -416,11 +416,11 @@
     val (lhss, rhss) = split_list eqs;
     val sort = fp_sort lhss (SOME resBs);
     fun qualify b = Binding.qualify true (Binding.name_of (Binding.prefix_name rawN b));
-    val ((bnfs, (Dss, Ass)), (unfold, lthy')) = apfst (apsnd split_list o split_list)
+    val ((bnfs, (Dss, Ass)), (unfold_set, lthy')) = apfst (apsnd split_list o split_list)
       (fold_map2 (fn b => bnf_of_typ Smart_Inline (qualify b) sort) bs rhss
-        (empty_unfold, lthy));
+        (empty_unfolds, lthy));
   in
-    mk_fp_bnf timer (construct mixfixes) (SOME resBs) bs sort lhss bnfs Dss Ass unfold lthy'
+    mk_fp_bnf timer (construct mixfixes) (SOME resBs) bs sort lhss bnfs Dss Ass unfold_set lthy'
   end;
 
 fun fp_bnf_cmd construct (bs, (raw_lhss, raw_bnfs)) lthy =
@@ -429,12 +429,13 @@
     val lhss = map (dest_TFree o Syntax.read_typ lthy) raw_lhss;
     val sort = fp_sort lhss NONE;
     fun qualify b = Binding.qualify true (Binding.name_of (Binding.prefix_name rawN b));
-    val ((bnfs, (Dss, Ass)), (unfold, lthy')) = apfst (apsnd split_list o split_list)
+    val ((bnfs, (Dss, Ass)), (unfold_set, lthy')) = apfst (apsnd split_list o split_list)
       (fold_map2 (fn b => fn rawT =>
         (bnf_of_typ Smart_Inline (qualify b) sort (Syntax.read_typ lthy rawT)))
-      bs raw_bnfs (empty_unfold, lthy));
+      bs raw_bnfs (empty_unfolds, lthy));
   in
-    snd (mk_fp_bnf timer (construct (map (K NoSyn) bs)) NONE bs sort lhss bnfs Dss Ass unfold lthy')
+    snd (mk_fp_bnf timer
+      (construct (map (K NoSyn) bs)) NONE bs sort lhss bnfs Dss Ass unfold_set lthy')
   end;
 
 end;

--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Fri Sep 21 15:53:29 2012 +0200
@@ -443,9 +443,9 @@
 
             val [iter_def, rec_def] = map (Morphism.thm phi) defs;
 
-            val [iter, recx] = map (mk_iter_like As Cs o Morphism.term phi) csts;
+            val [iterx, recx] = map (mk_iter_like As Cs o Morphism.term phi) csts;
           in
-            ((wrap_res, ctrs, iter, recx, xss, ctr_defs, iter_def, rec_def), lthy)
+            ((wrap_res, ctrs, iterx, recx, xss, ctr_defs, iter_def, rec_def), lthy)
           end;
 
         fun define_coiter_corec (wrap_res, no_defs_lthy) =

--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Fri Sep 21 15:53:29 2012 +0200
@@ -1051,7 +1051,7 @@
 
     val iter_fun = Term.absfree iter_f'
       (mk_mor UNIVs ctors active_UNIVs ss (map (mk_nthN n iter_f) ks));
-    val iter = HOLogic.choice_const iterT $ iter_fun;
+    val iterx = HOLogic.choice_const iterT $ iter_fun;
 
     fun iter_bind i = Binding.suffix_name ("_" ^ ctor_iterN) (nth bs (i - 1));
     val iter_name = Binding.name_of o iter_bind;
@@ -1062,7 +1062,7 @@
         val iterT = Library.foldr (op -->) (sTs, T --> AT);
 
         val lhs = Term.list_comb (Free (iter_name i, iterT), ss);
-        val rhs = mk_nthN n iter i;
+        val rhs = mk_nthN n iterx i;
       in
         mk_Trueprop_eq (lhs, rhs)
       end;
@@ -1175,9 +1175,9 @@
           mk_Trueprop_eq (HOLogic.mk_comp (dtor, ctor), HOLogic.id_const FT);
         val goals = map3 mk_goal dtors ctors FTs;
       in
-        map5 (fn goal => fn dtor_def => fn iter => fn map_comp_id => fn map_congL =>
+        map5 (fn goal => fn dtor_def => fn iterx => fn map_comp_id => fn map_congL =>
           Skip_Proof.prove lthy [] [] goal
-            (K (mk_dtor_o_ctor_tac dtor_def iter map_comp_id map_congL ctor_o_iter_thms))
+            (K (mk_dtor_o_ctor_tac dtor_def iterx map_comp_id map_congL ctor_o_iter_thms))
           |> Thm.close_derivation)
         goals dtor_defs iter_thms map_comp_id_thms map_congL_thms
       end;
@@ -1256,8 +1256,8 @@
           end;
         val goals = map5 mk_goal ks rec_ss rec_maps_rev ctors xFs;
       in
-        map2 (fn goal => fn iter =>
-          Skip_Proof.prove lthy [] [] goal (mk_rec_tac rec_defs iter fst_rec_pair_thms)
+        map2 (fn goal => fn iterx =>
+          Skip_Proof.prove lthy [] [] goal (mk_rec_tac rec_defs iterx fst_rec_pair_thms)
           |> Thm.close_derivation)
         goals iter_thms
       end;
@@ -1401,8 +1401,8 @@
                 HOLogic.mk_comp (ctor', Term.list_comb (map, fs @ fs_maps))));
             val goals = map4 mk_goal fs_maps map_FTFT's ctors ctor's;
             val maps =
-              map4 (fn goal => fn iter => fn map_comp_id => fn map_cong =>
-                Skip_Proof.prove lthy [] [] goal (K (mk_map_tac m n iter map_comp_id map_cong))
+              map4 (fn goal => fn iterx => fn map_comp_id => fn map_cong =>
+                Skip_Proof.prove lthy [] [] goal (K (mk_map_tac m n iterx map_comp_id map_cong))
                 |> Thm.close_derivation)
               goals iter_thms map_comp_id_thms map_congs;
           in
@@ -1461,8 +1461,8 @@
                 HOLogic.mk_comp (col, Term.list_comb (map, passive_ids @ sets)));
             val goalss =
               map3 (fn sets => map4 (mk_goal sets) ctors sets) setss_by_range colss map_setss;
-            val setss = map (map2 (fn iter => fn goal =>
-              Skip_Proof.prove lthy [] [] goal (K (mk_set_tac iter)) |> Thm.close_derivation)
+            val setss = map (map2 (fn iterx => fn goal =>
+              Skip_Proof.prove lthy [] [] goal (K (mk_set_tac iterx)) |> Thm.close_derivation)
               iter_thms) goalss;
 
             fun mk_simp_goal pas_set act_sets sets ctor z set =

--- a/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML	Fri Sep 21 15:53:29 2012 +0200
@@ -514,17 +514,17 @@
     CONJ_WRAP' mk_unique type_defs 1
   end;
 
-fun mk_dtor_o_ctor_tac dtor_def iter map_comp_id map_congL ctor_o_iters =
-  EVERY' [stac dtor_def, rtac ext, rtac trans, rtac o_apply, rtac trans, rtac iter,
+fun mk_dtor_o_ctor_tac dtor_def iterx map_comp_id map_congL ctor_o_iters =
+  EVERY' [stac dtor_def, rtac ext, rtac trans, rtac o_apply, rtac trans, rtac iterx,
     rtac trans, rtac map_comp_id, rtac trans, rtac map_congL,
     EVERY' (map (fn thm => rtac ballI THEN' rtac (trans OF [thm RS fun_cong, id_apply]))
       ctor_o_iters),
     rtac sym, rtac id_apply] 1;
 
-fun mk_rec_tac rec_defs iter fst_recs {context = ctxt, prems = _}=
+fun mk_rec_tac rec_defs iterx fst_recs {context = ctxt, prems = _}=
   unfold_defs_tac ctxt
     (rec_defs @ map (fn thm => thm RS @{thm convol_expand_snd}) fst_recs) THEN
-  EVERY' [rtac trans, rtac o_apply, rtac trans, rtac (iter RS @{thm arg_cong[of _ _ snd]}),
+  EVERY' [rtac trans, rtac o_apply, rtac trans, rtac (iterx RS @{thm arg_cong[of _ _ snd]}),
     rtac @{thm snd_convol'}] 1;
 
 fun mk_ctor_induct_tac m set_natural'ss init_induct morEs mor_Abs Rep_invs Abs_invs Reps =
@@ -570,8 +570,8 @@
       CONJ_WRAP' (K atac) ks] 1
   end;
 
-fun mk_map_tac m n iter map_comp_id map_cong =
-  EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, rtac iter, rtac trans, rtac o_apply,
+fun mk_map_tac m n iterx map_comp_id map_cong =
+  EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, rtac iterx, rtac trans, rtac o_apply,
     rtac trans, rtac (map_comp_id RS arg_cong), rtac trans, rtac (map_cong RS arg_cong),
     REPEAT_DETERM_N m o rtac refl,
     REPEAT_DETERM_N n o (EVERY' (map rtac [trans, o_apply, id_apply])),
@@ -591,8 +591,8 @@
       CONJ_WRAP' mk_mor (map_comp_ids ~~ map_congs)] 1
   end;
 
-fun mk_set_tac iter = EVERY' [rtac ext, rtac trans, rtac o_apply,
-  rtac trans, rtac iter, rtac sym, rtac o_apply] 1;
+fun mk_set_tac iterx = EVERY' [rtac ext, rtac trans, rtac o_apply,
+  rtac trans, rtac iterx, rtac sym, rtac o_apply] 1;
 
 fun mk_set_simp_tac set set_natural' set_natural's =
   let