# HG changeset patch
# User blanchet
# Date 1410177815 -7200
# Node ID 0ea19fc3b9576cd5e2375362be2ead977f57757b
# Parent  5451c61ee186d2057cfc4a0e68254cedcfc2d643
improved caching

diff -r 5451c61ee186 -r 0ea19fc3b957 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Sep 08 14:03:13 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Mon Sep 08 14:03:35 2014 +0200
@@ -104,8 +104,12 @@
       case f x of SOME y => (y :: ys, (x :: good, bad)) | NONE => (ys, (good, x :: bad)))
     xs ([], ([], []));
 
-fun key_of_fp_eqs fp fpTs fp_eqs =
-  Type (case_fp fp "l" "g", fpTs @ maps (fn (x, T) => [TFree x, T]) fp_eqs);
+fun key_of_fp_eqs fp As fpTs fp_eqs =
+  Type (case_fp fp "l" "g", fpTs @ maps (fn (x, T) => [TFree x, T]) fp_eqs)
+  |> Term.map_atyps (fn T as TFree (_, S) =>
+    (case find_index (curry (op =) T) As of
+      ~1 => T
+    | j => TFree ("'" ^ string_of_int j, S)));
 
 fun get_indices callers t =
   callers
@@ -202,7 +206,7 @@
     val mss = map (map length) ctr_Tsss;
 
     val fp_eqs = map dest_TFree Xs ~~ ctrXs_repTs;
-    val key = key_of_fp_eqs fp fpTs fp_eqs;
+    val key = key_of_fp_eqs fp As fpTs fp_eqs;
   in
     (case n2m_sugar_of no_defs_lthy key of
       SOME n2m_sugar => (n2m_sugar, no_defs_lthy)
@@ -375,9 +379,8 @@
 
           fun fresh_tyargs () =
             let
-              (* The name "'zy" is unlikely to clash with the context, yielding more cache hits. *)
               val (gen_tyargs, lthy') =
-                variant_tfrees (replicate (length tyargs) "zy") lthy
+                variant_tfrees (replicate (length tyargs) "a") lthy
                 |>> map Logic.varifyT_global;
               val rho' = (gen_tyargs ~~ tyargs) @ rho;
             in