# HG changeset patch
# User berghofe
# Date 1485686988 -3600
# Node ID d19a5579ffb8737f04b664aeac5de77a31f1c379
# Parent  8be78855ee7adfc17edbe4dc432461a2fae0baa4
Corrected type of dummy pattern

diff -r 8be78855ee7a -r d19a5579ffb8 src/HOL/Tools/Ctr_Sugar/case_translation.ML
--- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Sat Jan 28 15:12:19 2017 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Sun Jan 29 11:49:48 2017 +0100
@@ -498,18 +498,18 @@
           SOME (_, constructors) =>
             if length fs = length constructors then
               let
+                val R = fastype_of x;
                 val cases = map (fn (Const (s, U), t) =>
                   let
                     val Us = binder_types U;
                     val k = length Us;
                     val p as (xs, _) = strip_abs k t;
                   in
-                    (Const (s, map fastype_of xs ---> fastype_of x), p, is_dependent k t)
+                    (Const (s, map fastype_of xs ---> R), p, is_dependent k t)
                   end) (constructors ~~ fs);
                 val cases' =
                   sort (int_ord o swap o apply2 (length o snd))
                     (fold_rev count_cases cases []);
-                val R = fastype_of t;
                 val dummy =
                   if d then Term.dummy_pattern R
                   else Free (Name.variant "x" used |> fst, R);