merged
authorwenzelm
Wed, 10 Apr 2013 20:06:36 +0200
changeset 51690 c85409ead923
parent 51684 0b5497bdaddf (diff)
parent 51689 43a3465805dd (current diff)
child 51691 69e3bc394f09
merged
--- a/src/HOL/Tools/case_translation.ML	Wed Apr 10 19:14:47 2013 +0200
+++ b/src/HOL/Tools/case_translation.ML	Wed Apr 10 20:06:36 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;