1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon May 06 15:10:21 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon May 06 18:17:45 2013 +0200
     1.3 @@ -199,7 +199,7 @@
     1.4  val mk_ctor = mk_ctor_or_dtor range_type;
     1.5  val mk_dtor = mk_ctor_or_dtor domain_type;
     1.6  
     1.7 -fun mk_xxiter lfp Ts Us t =
     1.8 +fun mk_co_iter lfp Ts Us t =
     1.9    let
    1.10      val (bindings, body) = strip_type (fastype_of t);
    1.11      val (f_Us, prebody) = split_last bindings;
    1.12 @@ -212,7 +212,7 @@
    1.13  val mk_fp_iter_fun_types = fst o split_last o binder_types o fastype_of;
    1.14  
    1.15  fun mk_fp_iter lfp As Cs fp_iters0 =
    1.16 -  map (mk_xxiter lfp As Cs) fp_iters0
    1.17 +  map (mk_co_iter lfp As Cs) fp_iters0
    1.18    |> (fn ts => (ts, mk_fp_iter_fun_types (hd ts)));
    1.19  
    1.20  fun unzip_recT fpTs T =
    1.21 @@ -1216,7 +1216,7 @@
    1.22  
    1.23              val [fold_def, rec_def] = map (Morphism.thm phi) defs;
    1.24  
    1.25 -            val [foldx, recx] = map (mk_xxiter lfp As Cs o Morphism.term phi) csts;
    1.26 +            val [foldx, recx] = map (mk_co_iter lfp As Cs o Morphism.term phi) csts;
    1.27            in
    1.28              ((foldx, recx, fold_def, rec_def), lthy')
    1.29            end;
    1.30 @@ -1266,13 +1266,13 @@
    1.31  
    1.32              val [unfold_def, corec_def] = map (Morphism.thm phi) defs;
    1.33  
    1.34 -            val [unfold, corec] = map (mk_xxiter lfp As Cs o Morphism.term phi) csts;
    1.35 +            val [unfold, corec] = map (mk_co_iter lfp As Cs o Morphism.term phi) csts;
    1.36            in
    1.37              ((unfold, corec, unfold_def, corec_def), lthy')
    1.38            end;
    1.39  
    1.40 -        fun massage_res (((maps_sets_rels, ctr_sugar), xxiter_res), lthy) =
    1.41 -          (((maps_sets_rels, (ctrs, xss, ctr_defs, ctr_sugar)), xxiter_res), lthy);
    1.42 +        fun massage_res (((maps_sets_rels, ctr_sugar), co_iter_res), lthy) =
    1.43 +          (((maps_sets_rels, (ctrs, xss, ctr_defs, ctr_sugar)), co_iter_res), lthy);
    1.44        in
    1.45          (wrap
    1.46           #> derive_maps_sets_rels