1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Wed Sep 25 16:43:46 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Wed Sep 25 16:52:51 2013 +0200
     1.3 @@ -266,20 +266,23 @@
     1.4            end
     1.5          | (Const (c, _), args as _ :: _) =>
     1.6            let val n = num_binder_types (Sign.the_const_type thy c) in
     1.7 -            (case fastype_of1 (bound_Ts, nth args (n - 1)) of
     1.8 -              Type (s, Ts) =>
     1.9 -              if case_of ctxt s = SOME c then
    1.10 -                let
    1.11 -                  val (branches, obj_leftovers) = chop n args;
    1.12 -                  val branches' = map (massage_rec bound_Ts) branches;
    1.13 -                  val casex' = Const (c, map typof branches' ---> map typof obj_leftovers --->
    1.14 -                    typof t);
    1.15 -                in
    1.16 -                  betapplys (casex', branches' @ tap (List.app check_no_call) obj_leftovers)
    1.17 -                end
    1.18 -              else
    1.19 -                massage_leaf bound_Ts t
    1.20 -            | _ => massage_leaf bound_Ts t)
    1.21 +            if length args >= n then
    1.22 +              (case fastype_of1 (bound_Ts, nth args (n - 1)) of
    1.23 +                Type (s, Ts) =>
    1.24 +                if case_of ctxt s = SOME c then
    1.25 +                  let
    1.26 +                    val (branches, obj_leftovers) = chop n args;
    1.27 +                    val branches' = map (massage_rec bound_Ts) branches;
    1.28 +                    val casex' = Const (c, map typof branches' ---> map typof obj_leftovers --->
    1.29 +                      typof t);
    1.30 +                  in
    1.31 +                    betapplys (casex', branches' @ tap (List.app check_no_call) obj_leftovers)
    1.32 +                  end
    1.33 +                else
    1.34 +                  massage_leaf bound_Ts t
    1.35 +              | _ => massage_leaf bound_Ts t)
    1.36 +            else
    1.37 +              massage_leaf bound_Ts t
    1.38            end
    1.39          | _ => massage_leaf bound_Ts t)
    1.40        end