fixed off-by-one bug
authorblanchet
Wed, 25 Sep 2013 17:11:17 +0200
changeset 53894 4cb6be538b40
parent 53893 865da57dee93
child 53895 d2d93b736e56
fixed off-by-one bug
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