# HG changeset patch
# User blanchet
# Date 1346925880 -7200
# Node ID b8517107ffc59b15cdee108e0fcf878d1acbcab5
# Parent  64764f0efe802ea12305eeee0b3c32d2f048f5c0
read the real types off the constant types, rather than using the fake parser types (second step of sugar localization)

diff -r 64764f0efe80 -r b8517107ffc5 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Thu Sep 06 11:57:36 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Thu Sep 06 12:04:40 2012 +0200
@@ -67,12 +67,12 @@
 
     val N = length specs;
 
-    fun mk_T b =
+    fun mk_fake_T b =
       Type (fst (Term.dest_Type (Proof_Context.read_type_name fake_lthy true (Binding.name_of b))),
         As);
 
     val bs = map type_binder_of specs;
-    val fp_Ts = map mk_T bs;
+    val fake_Ts = map mk_fake_T bs;
 
     val mixfixes = map mixfix_of specs;
 
@@ -107,7 +107,7 @@
       | is_same_recT _ _ = false;
 
     fun freeze_recXs (T as Type (s, Us)) =
-        (case find_index (is_same_recT T) fp_Ts of
+        (case find_index (is_same_recT T) fake_Ts of
           ~1 => Type (s, map freeze_recXs Us)
         | i => nth Xs i)
       | freeze_recXs T = T;
@@ -133,6 +133,8 @@
     val unfs = map (mk_unf As) raw_unfs;
     val flds = map (mk_fld As) raw_flds;
 
+    val fp_Ts = map (domain_type o fastype_of) unfs;
+
     fun mk_fp_iter_or_rec Ts Us t =
       let
         val (binders, body) = strip_type (fastype_of t);