author | wenzelm |
Wed, 17 Jun 2009 17:07:26 +0200 | |
changeset 31689 | 84a14d2dc868 |
parent 31688 | f27cc190083b |
child 31692 | 57715a08e4b6 |
--- a/src/HOL/Tools/datatype_package/datatype_package.ML Wed Jun 17 17:07:26 2009 +0200 +++ b/src/HOL/Tools/datatype_package/datatype_package.ML Wed Jun 17 17:07:26 2009 +0200 @@ -351,7 +351,7 @@ simps : thm list} structure DatatypeInterpretation = InterpretationFun - (type T = datatype_config * string list val eq = eq_snd op =); + (type T = datatype_config * string list val eq: T * T -> bool = eq_snd op =); fun interpretation f = DatatypeInterpretation.interpretation (uncurry f);