# HG changeset patch
# User traytel
# Date 1404205591 -7200
# Node ID 2d0cf40f6fb3c9754796d5242fc2322963504bbc
# Parent  a26c39b95ceeebf10a65a09e7ce3f7fa2a38f985
generate type correct terms in uncheck phase

diff -r a26c39b95cee -r 2d0cf40f6fb3 src/HOL/Tools/Ctr_Sugar/case_translation.ML
--- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Mon Jun 30 15:23:00 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Tue Jul 01 11:06:31 2014 +0200
@@ -540,7 +540,8 @@
 
 fun encode_clause recur S T (pat, rhs) =
   fold (fn x as (_, U) => fn t =>
-    Const (@{const_name case_abs}, (U --> T) --> T) $ Term.absfree x t)
+    let val T = fastype_of t;
+    in Const (@{const_name case_abs}, (U --> T) --> T) $ Term.absfree x t end)
       (Term.add_frees pat [])
       (Const (@{const_name case_elem}, S --> T --> S --> T) $ pat $ recur rhs);