# HG changeset patch
# User blanchet
# Date 1380205054 -7200
# Node ID b19d300db73b3fcd0d8af7b8535cadd0dc5d6ec4
# Parent  7b43d22accc33d79d24de57606d1c17fe032bd73
avoid calls to nth with ~1

diff -r 7b43d22accc3 -r b19d300db73b src/HOL/BNF/Tools/bnf_ctr_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Thu Sep 26 16:10:57 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Thu Sep 26 16:17:34 2013 +0200
@@ -252,16 +252,20 @@
     (case ctr_sugar_of ctxt s of
       SOME {casex = Const (case_name, _), discs = discs0, selss = selss0, ...} =>
       if case_name = c then
-        let
-          val n = length discs0;
-          val (branches, obj :: leftovers) = chop n args;
-          val discs = map (mk_disc_or_sel Ts) discs0;
-          val selss = map (map (mk_disc_or_sel Ts)) selss0;
-          val conds = map (rapp obj) discs;
-          val branch_argss = map (fn sels => map (rapp obj) sels @ leftovers) selss;
-          val branches' = map2 (curry Term.betapplys) branches branch_argss;
-        in
-          SOME (conds, branches')
+        let val n = length discs0 in
+          if n < length args then
+            let
+              val (branches, obj :: leftovers) = chop n args;
+              val discs = map (mk_disc_or_sel Ts) discs0;
+              val selss = map (map (mk_disc_or_sel Ts)) selss0;
+              val conds = map (rapp obj) discs;
+              val branch_argss = map (fn sels => map (rapp obj) sels @ leftovers) selss;
+              val branches' = map2 (curry Term.betapplys) branches branch_argss;
+            in
+              SOME (conds, branches')
+            end
+          else
+            NONE
         end
       else
         NONE
diff -r 7b43d22accc3 -r b19d300db73b src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Sep 26 16:10:57 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Sep 26 16:17:34 2013 +0200
@@ -234,7 +234,7 @@
         o fld (conds @ s_not_disj cond) else_branch
       | (Const (c, _), args as _ :: _ :: _) =>
         let val n = num_binder_types (Sign.the_const_type thy c) - 1 in
-          if length args > n then
+          if n >= 0 andalso n < length args then
             (case fastype_of1 (bound_Ts, nth args n) of
               Type (s, Ts) =>
               (case dest_case ctxt s Ts t of
@@ -276,7 +276,7 @@
             val (gen_branch_Ts, gen_body_fun_T) = strip_fun_type gen_T;
             val n = length gen_branch_Ts;
           in
-            if length args > n then
+            if n < length args then
               (case gen_body_fun_T of
                 Type (_, [Type (T_name, _), _]) =>
                 if case_of ctxt T_name = SOME c then