# HG changeset patch
# User blanchet
# Date 1383626888 -3600
# Node ID d1478807f287721dada865e23187c6da02239429
# Parent  04cd231e2b9e396bee840619e0defe7a32b73335
generalize types when synthetizing n2m (co)recursors, to facilitate reuse

diff -r 04cd231e2b9e -r d1478807f287 src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Tue Nov 05 05:48:08 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Tue Nov 05 05:48:08 2013 +0100
@@ -295,10 +295,19 @@
       | check_enrich_with_mutuals _ (T :: _) = not_co_datatype T;
 
     val perm_Ts = check_enrich_with_mutuals [] perm_actual_Ts;
-
     val missing_Ts = perm_Ts |> subtract (op =) actual_Ts;
     val Ts = actual_Ts @ missing_Ts;
 
+    fun generalize_type (T as Type (s, Ts)) (seen_lthy as (seen, lthy)) =
+        (case AList.lookup (op =) seen T of
+          SOME U => (U, seen_lthy)
+        | NONE =>
+          if exists_subtype_in Ts T then fold_map generalize_type Ts seen_lthy |>> curry Type s
+          else mk_TFrees 1 lthy |> (fn ([U], lthy) => (U, ((T, U) :: seen, lthy))))
+      | generalize_type T seen_lthy = (T, seen_lthy);
+
+    val (perm_Us, _) = fold_map generalize_type perm_Ts ([], lthy);
+
     val nn = length Ts;
     val kks = 0 upto nn - 1;
 
@@ -318,7 +327,7 @@
     val get_perm_indices = map (fn kk => find_index (curry (op =) kk) perm_kks) o get_indices;
 
     val ((perm_fp_sugars, fp_sugar_thms), lthy) =
-      mutualize_fp_sugars has_nested fp perm_bs perm_Ts get_perm_indices perm_callssss
+      mutualize_fp_sugars has_nested fp perm_bs perm_Us get_perm_indices perm_callssss
         perm_fp_sugars0 lthy;
 
     val fp_sugars = unpermute perm_fp_sugars;