# HG changeset patch
# User traytel
# Date 1409740225 -7200
# Node ID df15198c6309b0a2e3639b6ed444b1940c40571f
# Parent  deeff89d5b9ec5b6c92a3da0f02d1165c015e512
lessen the burden on the caller: sort where necessary in n2m

diff -r deeff89d5b9e -r df15198c6309 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)))