lessen the burden on the caller: sort where necessary in n2m
authortraytel
Wed, 03 Sep 2014 12:30:25 +0200
changeset 58162 df15198c6309
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
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Sep 03 09:43:00 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Sep 03 12:30:25 2014 +0200
@@ -268,7 +268,8 @@
         val fold_preTs' = mk_fp_absT_repTs (map subst fold_preTs);
 
         val fold_pre_deads_only_Ts =
-          map (typ_subst_nonatomic_sorted (map (rpair dummyT) (As @ fpTs))) fold_preTs';
+          map (typ_subst_nonatomic_sorted (map (rpair dummyT)
+            (As @ sort (int_ord o pairself Term.size_of_typ) fpTs))) fold_preTs';
 
         val (clique, TUs) =
           map_split dest_co_algT (binder_fun_types (foldT_of_recT (fastype_of approx_rec)))