stronger normalization, to increase n2m cache effectiveness
authorblanchet
Tue, 05 Nov 2013 11:55:45 +0100
changeset 54266 4e0738356ac9
parent 54265 3e1d230f1c00
child 54267 78e8a178b690
stronger normalization, to increase n2m cache effectiveness
src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Tue Nov 05 11:17:42 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Tue Nov 05 11:55:45 2013 +0100
@@ -307,7 +307,7 @@
     val _ = (case Library.duplicates (op =) actual_Ts of [] => () | T :: _ => duplicate_datatype T);
 
     val perm_actual_Ts as Type (_, ty_args0) :: _ =
-      sort (int_ord o pairself Term.size_of_typ) actual_Ts;
+      sort (prod_ord int_ord Term_Ord.typ_ord o pairself (`Term.size_of_typ)) actual_Ts;
 
     fun check_enrich_with_mutuals _ [] = []
       | check_enrich_with_mutuals seen ((T as Type (T_name, ty_args)) :: Ts) =
@@ -332,8 +332,9 @@
     val missing_Ts = perm_Ts |> subtract (op =) actual_Ts;
     val Ts = actual_Ts @ missing_Ts;
 
+    (* The name "'z" is likely not to clash with the context, resulting in more cache hits. *)
     fun generalize_simple_type T (seen, lthy) =
-      variant_tfrees ["aa"] lthy |> (fn ([U], lthy) => (U, ((T, U) :: seen, lthy)));
+      variant_tfrees ["z"] lthy |> (fn ([U], lthy) => (U, ((T, U) :: seen, lthy)));
 
     fun generalize_type T (seen_lthy as (seen, _)) =
       (case AList.lookup (op =) seen T of