reverted too aggressive 7cb8442298f0

--- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Wed Nov 06 01:06:01 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Wed Nov 06 01:57:22 2013 +0100
@@ -330,18 +330,21 @@
     val missing_Ts = perm_Ts |> subtract (op =) actual_Ts;
     val Ts = actual_Ts @ missing_Ts;
 
-    fun generalize_subtype T (tyarps_lthy as (tyarps, lthy)) =
-      (* The name "'z" is unlikely to clash with the context, resulting in more cache hits. *)
-      if exists_subtype_in Ts T then generalize_Type T tyarps_lthy
-      else variant_tfrees ["z"] lthy |> (fn ([U], lthy) => (U, (tyarps, lthy)))
-    and generalize_Type (Type (s, tyargs)) (tyarps_lthy as (tyarps, _)) =
-      (case AList.lookup (op =) tyarps tyargs of
-        SOME tyargs' => (Type (s, tyargs'), tyarps_lthy)
-      | NONE => fold_map generalize_subtype tyargs tyarps_lthy
-        |> (fn (tyargs', (tyarps, lthy)) =>
-          (Type (s, tyargs'), ((tyargs, tyargs') :: tyarps, lthy))));
+    (* 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 ["z"] lthy |> (fn ([U], lthy) => (U, ((T, U) :: seen, lthy)));
 
-    val (perm_Us, _) = fold_map generalize_Type perm_Ts ([], lthy);
+    fun generalize_type T (seen_lthy as (seen, _)) =
+      (case AList.lookup (op =) seen T of
+        SOME U => (U, seen_lthy)
+      | NONE =>
+        (case T of
+          Type (s, tyargs) =>
+          if exists_subtype_in Ts T then fold_map generalize_type tyargs seen_lthy |>> curry Type s
+          else generalize_simple_type T seen_lthy
+        | _ => generalize_simple_type T seen_lthy));
+
+    val (perm_Us, _) = fold_map generalize_type perm_Ts ([], lthy);
 
     val nn = length Ts;
     val kks = 0 upto nn - 1;