# HG changeset patch
# User traytel
# Date 1365616339 -7200
# Node ID 0b5497bdaddf65723aa1db549dea43819ac11cd3
# Parent  baefa3b461c2531f0c2a39c37853f06e743b28c2
made SML/NJ happy

diff -r baefa3b461c2 -r 0b5497bdaddf src/HOL/Tools/case_translation.ML
--- a/src/HOL/Tools/case_translation.ML	Wed Apr 10 18:51:21 2013 +0200
+++ b/src/HOL/Tools/case_translation.ML	Wed Apr 10 19:52:19 2013 +0200
@@ -53,7 +53,7 @@
 
 val rep_data = (fn Data args => args) o Data.get o Context.Proof;
 
-fun T_of_data (comb, constrs) =
+fun T_of_data (comb, constrs : term list) =
   fastype_of comb
   |> funpow (length constrs) range_type
   |> domain_type;