# HG changeset patch
# User traytel
# Date 1440192472 -7200
# Node ID 151d923326253f73ba6a07089d38359335ae5438
# Parent  1dd6669ff612944aea1c373876cca4f05520a472# Parent  0b9d8af732700432dcf8dd955f79bfd4552f2acb
merged

diff -r 0b9d8af73270 -r 151d92332625 src/HOL/Tools/Ctr_Sugar/case_translation.ML
--- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Fri Aug 21 22:11:55 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Fri Aug 21 23:27:52 2015 +0200
@@ -470,12 +470,13 @@
     (SOME cname, ts as _ :: _) =>
       let
         val (fs, x) = split_last ts;
-        fun strip_abs i Us t =
+        fun strip_abs i t =
           let
             val zs = strip_abs_vars t;
             val j = length zs;
             val (xs, ys) =
-              if j < i then (zs @ map (pair "x") (drop j Us), [])
+              if j < i then (zs @
+                map (pair "x") (drop j (take i (binder_types (fastype_of t)))), [])
               else chop i zs;
             val u = fold_rev Term.abs ys (strip_abs_body t);
             val xs' = map Free
@@ -501,7 +502,7 @@
                   let
                     val Us = binder_types U;
                     val k = length Us;
-                    val p as (xs, _) = strip_abs k Us t;
+                    val p as (xs, _) = strip_abs k t;
                   in
                     (Const (s, map fastype_of xs ---> fastype_of x), p, is_dependent k t)
                   end) (constructors ~~ fs);