lessen the burden on the caller: sort where necessary in n2m
authortraytel
Wed Sep 03 12:30:25 2014 +0200 (2014-09-03)
changeset 58162df15198c6309
parent 58161 deeff89d5b9e
child 58163 c1e32fe387f4
lessen the burden on the caller: sort where necessary in n2m
src/HOL/Tools/BNF/bnf_fp_n2m.ML
     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)))