# HG changeset patch
# User blanchet
# Date 1367857065 -7200
# Node ID 7a2eb7f989afa15c8a37f0b41a8890c9d1a4f2a0
# Parent  2023639f566bbeb8bec3b58dcedcd11507381acc
tuning

diff -r 2023639f566b -r 7a2eb7f989af src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon May 06 15:10:21 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon May 06 18:17:45 2013 +0200
@@ -199,7 +199,7 @@
 val mk_ctor = mk_ctor_or_dtor range_type;
 val mk_dtor = mk_ctor_or_dtor domain_type;
 
-fun mk_xxiter lfp Ts Us t =
+fun mk_co_iter lfp Ts Us t =
   let
     val (bindings, body) = strip_type (fastype_of t);
     val (f_Us, prebody) = split_last bindings;
@@ -212,7 +212,7 @@
 val mk_fp_iter_fun_types = fst o split_last o binder_types o fastype_of;
 
 fun mk_fp_iter lfp As Cs fp_iters0 =
-  map (mk_xxiter lfp As Cs) fp_iters0
+  map (mk_co_iter lfp As Cs) fp_iters0
   |> (fn ts => (ts, mk_fp_iter_fun_types (hd ts)));
 
 fun unzip_recT fpTs T =
@@ -1216,7 +1216,7 @@
 
             val [fold_def, rec_def] = map (Morphism.thm phi) defs;
 
-            val [foldx, recx] = map (mk_xxiter lfp As Cs o Morphism.term phi) csts;
+            val [foldx, recx] = map (mk_co_iter lfp As Cs o Morphism.term phi) csts;
           in
             ((foldx, recx, fold_def, rec_def), lthy')
           end;
@@ -1266,13 +1266,13 @@
 
             val [unfold_def, corec_def] = map (Morphism.thm phi) defs;
 
-            val [unfold, corec] = map (mk_xxiter lfp As Cs o Morphism.term phi) csts;
+            val [unfold, corec] = map (mk_co_iter lfp As Cs o Morphism.term phi) csts;
           in
             ((unfold, corec, unfold_def, corec_def), lthy')
           end;
 
-        fun massage_res (((maps_sets_rels, ctr_sugar), xxiter_res), lthy) =
-          (((maps_sets_rels, (ctrs, xss, ctr_defs, ctr_sugar)), xxiter_res), lthy);
+        fun massage_res (((maps_sets_rels, ctr_sugar), co_iter_res), lthy) =
+          (((maps_sets_rels, (ctrs, xss, ctr_defs, ctr_sugar)), co_iter_res), lthy);
       in
         (wrap
          #> derive_maps_sets_rels