# HG changeset patch
# User blanchet
# Date 1380120771 -7200
# Node ID 27da6373a64f6fcc4bc7c2a0e0b99cca2a14c7f4
# Parent  5f647a5bd46e20d943005a312153b38066b97269
robustness

diff -r 5f647a5bd46e -r 27da6373a64f src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
--- 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