# HG changeset patch
# User blanchet
# Date 1380121877 -7200
# Node ID 4cb6be538b40e1725bf53035e4e7fc91e5fa0378
# Parent  865da57dee932430a3cbe7440707456e72d9f01b
fixed off-by-one bug

diff -r 865da57dee93 -r 4cb6be538b40 src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
--- 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