# HG changeset patch
# User blanchet
# Date 1346836098 -7200
# Node ID e32b1f74885452cebc24a174f8efe971309d62a2
# Parent  0f81eca1e47339ada7d84aa5c8f1e52ddeaa0d8b
added a check

diff -r 0f81eca1e473 -r e32b1f748854 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Wed Sep 05 10:53:51 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Wed Sep 05 11:08:18 2012 +0200
@@ -99,9 +99,14 @@
       |> mk_TFrees N
       ||> the_single o fst o mk_TFrees 1;
 
-    fun freeze_rec (T as Type (s, Ts')) =
-        (case find_index (curry (op =) T) Ts of
-          ~1 => Type (s, map freeze_rec Ts')
+    fun is_same_rec (T as Type (s, Us)) (Type (s', Us')) =
+        s = s' andalso (Us = Us' orelse error ("Illegal occurrence of recursive type " ^
+          quote (Syntax.string_of_typ fake_lthy T)))
+      | is_same_rec _ _ = false
+
+    fun freeze_rec (T as Type (s, Us)) =
+        (case find_index (is_same_rec T) Ts of
+          ~1 => Type (s, map freeze_rec Us)
         | i => nth Bs i)
       | freeze_rec T = T;
 
@@ -210,11 +215,17 @@
         fun sugar_lfp lthy =
           let
 (*###
-            val iter_Tss = map ( ) ctr_Tss
+            val fld_iter = @{term True}; (*###*)
+
+            val iter_Tss = map (fn Ts => Ts) (*###*) ctr_Tss;
             val iter_Ts = map (fn Ts => Ts ---> C) iter_Tss;
 
             val iter_fs = map2 (fn Free (s, _) => fn T => Free (s, T)) fs iter_Ts
 
+            val iter_rhs =
+              fold_rev Term.lambda fs (fld_iter $ mk_sum_caseN (uncurry_fs fs xss) $ (unf $ v));
+
+
             val uncurried_fs =
               map2 (fn f => fn xs =>
                 HOLogic.tupled_lambda (HOLogic.mk_tuple xs) (Term.list_comb (f, xs))) fs xss;