# HG changeset patch
# User blanchet
# Date 1347132087 -7200
# Node ID 6d8d5fe9f3a205b41c95ff4d3e9385e0818ad7aa
# Parent  a6260b4fb4103aab9cf5cf7c16c473c3179d4502
fixed bug with one-value types with phantom type arguments

diff -r a6260b4fb410 -r 6d8d5fe9f3a2 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 08 21:04:27 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 08 21:21:27 2012 +0200
@@ -222,6 +222,9 @@
         end
       else
         let
+          (*avoid "'a itself" arguments in coiterators and corecursors*)
+          val mss' =  map (fn [0] => [1] | ms => ms) mss;
+
           val p_Tss =
             map2 (fn C => fn n => replicate (Int.max (0, n - 1)) (C --> HOLogic.boolT)) Cs ns;
 
@@ -233,7 +236,7 @@
               val f_sum_prod_Ts = map range_type fun_Ts;
               val f_prod_Tss = map2 dest_sumTN ns f_sum_prod_Ts;
               val f_Tsss =
-                map3 (fn C => map2 (map (curry (op -->) C) oo dest_tupleT)) Cs mss f_prod_Tss;
+                map3 (fn C => map2 (map (curry (op -->) C) oo dest_tupleT)) Cs mss' f_prod_Tss;
               val pf_Tss = map2 popescu_zip p_Tss f_Tsss
             in (f_sum_prod_Ts, f_prod_Tss, f_Tsss, pf_Tss) end;