# HG changeset patch
# User blanchet
# Date 1383648945 -3600
# Node ID 4e0738356ac9be1b87a59c2a67ed779c5047cc27
# Parent  3e1d230f1c0067dc1a18b89b4eb595b18e096189
stronger normalization, to increase n2m cache effectiveness

diff -r 3e1d230f1c00 -r 4e0738356ac9 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