# HG changeset patch
# User wenzelm
# Date 1245251246 -7200
# Node ID 84a14d2dc86872109eabd19f3fa4ad244eef9e02
# Parent  f27cc190083b2d9ad6ade6d86bc71e2bb7163ff5
made SML/NJ happy;

diff -r f27cc190083b -r 84a14d2dc868 src/HOL/Tools/datatype_package/datatype_package.ML
--- 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);