--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Wed Sep 25 17:01:29 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Wed Sep 25 17:11:17 2013 +0200
@@ -267,9 +267,9 @@
Term.list_comb (If_const (typof (hd branches')) $ tap check_no_call obj, branches')
end
| (Const (c, _), args as _ :: _) =>
- let val n = num_binder_types (Sign.the_const_type thy c) in
- if length args >= n then
- (case fastype_of1 (bound_Ts, nth args (n - 1)) of
+ let val n = num_binder_types (Sign.the_const_type thy c) - 1 in
+ if n < length args then
+ (case fastype_of1 (bound_Ts, nth args n) of
Type (s, Ts) =>
if case_of ctxt s = SOME c then
let