| changeset 51684 | 0b5497bdaddf |
| parent 51681 | bdfa3b947992 |
| child 51692 | ecd34f863242 |
--- 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;