--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Wed Sep 25 16:43:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Wed Sep 25 16:52:51 2013 +0200
@@ -266,20 +266,23 @@
end
| (Const (c, _), args as _ :: _) =>
let val n = num_binder_types (Sign.the_const_type thy c) in
- (case fastype_of1 (bound_Ts, nth args (n - 1)) of
- Type (s, Ts) =>
- if case_of ctxt s = SOME c then
- let
- val (branches, obj_leftovers) = chop n args;
- val branches' = map (massage_rec bound_Ts) branches;
- val casex' = Const (c, map typof branches' ---> map typof obj_leftovers --->
- typof t);
- in
- betapplys (casex', branches' @ tap (List.app check_no_call) obj_leftovers)
- end
- else
- massage_leaf bound_Ts t
- | _ => massage_leaf bound_Ts t)
+ if length args >= n then
+ (case fastype_of1 (bound_Ts, nth args (n - 1)) of
+ Type (s, Ts) =>
+ if case_of ctxt s = SOME c then
+ let
+ val (branches, obj_leftovers) = chop n args;
+ val branches' = map (massage_rec bound_Ts) branches;
+ val casex' = Const (c, map typof branches' ---> map typof obj_leftovers --->
+ typof t);
+ in
+ betapplys (casex', branches' @ tap (List.app check_no_call) obj_leftovers)
+ end
+ else
+ massage_leaf bound_Ts t
+ | _ => massage_leaf bound_Ts t)
+ else
+ massage_leaf bound_Ts t
end
| _ => massage_leaf bound_Ts t)
end