diff -r 61729b149397 -r 902b24e0ffb4 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Oct 01 10:46:30 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Oct 01 11:04:30 2012 +0200
@@ -604,8 +604,8 @@
                   if s = s' then build_map (build_ctor_rec_arg mk_proj) T U else mk_proj T
                 | _ => mk_proj T);
 
-            fun mk_U proj (T as Type (@{type_name prod}, [T', U])) =
-                if member (op =) fpTs T' then proj (T', U) else T
+            fun mk_U proj (Type (s as @{type_name prod}, Ts as [T', U])) =
+                if member (op =) fpTs T' then proj (T', U) else Type (s, map (mk_U proj) Ts)
               | mk_U proj (Type (s, Ts)) = Type (s, map (mk_U proj) Ts)
               | mk_U _ T = T;