src/HOL/Tools/BNF/bnf_fp_n2m.ML
changeset 58162 df15198c6309
parent 57802 9c065009cd8a
child 58180 95397823f39e
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Sep 03 09:43:00 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Sep 03 12:30:25 2014 +0200
     1.3 @@ -268,7 +268,8 @@
     1.4          val fold_preTs' = mk_fp_absT_repTs (map subst fold_preTs);
     1.5  
     1.6          val fold_pre_deads_only_Ts =
     1.7 -          map (typ_subst_nonatomic_sorted (map (rpair dummyT) (As @ fpTs))) fold_preTs';
     1.8 +          map (typ_subst_nonatomic_sorted (map (rpair dummyT)
     1.9 +            (As @ sort (int_ord o pairself Term.size_of_typ) fpTs))) fold_preTs';
    1.10  
    1.11          val (clique, TUs) =
    1.12            map_split dest_co_algT (binder_fun_types (foldT_of_recT (fastype_of approx_rec)))