# HG changeset patch
# User blanchet
# Date 1379582852 -7200
# Node ID cfd6257331ca1ae323bc6dac2ab63cd28ed5eef8
# Parent  e2c0d0426d2b6c61f419fa56fb349bbc1843d02e
generalize code to handle zero-argument case gracefully (e.g. for nullay functions defined over codatatypes that corecurse through "fun"

diff -r e2c0d0426d2b -r cfd6257331ca src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Thu Sep 19 11:27:30 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Thu Sep 19 11:27:32 2013 +0200
@@ -586,18 +586,17 @@
     fun rewrite _ _ =
       let
         fun subst (Abs (v, T, b)) = Abs (v, T, subst b)
-          | subst (t as _ $ _) =
+          | subst t =
             let val (u, vs) = strip_comb t in
               if is_Free u andalso has_call u then
                 Const (@{const_name Inr}, dummyT) $
-                  (try (foldr1 (fn (x, y) => Const (@{const_name Pair}, dummyT) $ x $ y)) vs
-                    |> the_default (hd vs))
+                  (if null vs then HOLogic.unit
+                   else foldr1 (fn (x, y) => Const (@{const_name Pair}, dummyT) $ x $ y) vs)
               else if try (fst o dest_Const) u = SOME @{const_name prod_case} then
                 list_comb (u |> map_types (K dummyT), map subst vs)
               else
                 list_comb (subst u, map subst vs)
-            end
-          | subst t = t;
+            end;
       in
         subst
       end;