1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Thu Sep 19 11:27:30 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Thu Sep 19 11:27:32 2013 +0200
     1.3 @@ -586,18 +586,17 @@
     1.4      fun rewrite _ _ =
     1.5        let
     1.6          fun subst (Abs (v, T, b)) = Abs (v, T, subst b)
     1.7 -          | subst (t as _ $ _) =
     1.8 +          | subst t =
     1.9              let val (u, vs) = strip_comb t in
    1.10                if is_Free u andalso has_call u then
    1.11                  Const (@{const_name Inr}, dummyT) $
    1.12 -                  (try (foldr1 (fn (x, y) => Const (@{const_name Pair}, dummyT) $ x $ y)) vs
    1.13 -                    |> the_default (hd vs))
    1.14 +                  (if null vs then HOLogic.unit
    1.15 +                   else foldr1 (fn (x, y) => Const (@{const_name Pair}, dummyT) $ x $ y) vs)
    1.16                else if try (fst o dest_Const) u = SOME @{const_name prod_case} then
    1.17                  list_comb (u |> map_types (K dummyT), map subst vs)
    1.18                else
    1.19                  list_comb (subst u, map subst vs)
    1.20 -            end
    1.21 -          | subst t = t;
    1.22 +            end;
    1.23        in
    1.24          subst
    1.25        end;