# HG changeset patch
# User traytel
# Date 1440166211 -7200
# Node ID 1dd6669ff612944aea1c373876cca4f05520a472
# Parent  531a48ae14259ad1872763fb204332d61668c18c
don't use types that come from the database---they are inconsistent with the ones occurring in the terms

diff -r 531a48ae1425 -r 1dd6669ff612 src/HOL/Tools/Ctr_Sugar/case_translation.ML
--- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Thu Aug 20 21:14:58 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Fri Aug 21 16:10:11 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);