Added type constraint to make SML/NJ happy.
authorberghofe
Wed, 27 Oct 2004 10:30:07 +0200
changeset 15265 a1547232fedd
parent 15264 a881ad2e9edc
child 15266 0398af5501fe
Added type constraint to make SML/NJ happy.
src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Tue Oct 26 16:34:19 2004 +0200
+++ b/src/HOL/Tools/typedef_package.ML	Wed Oct 27 10:30:07 2004 +0200
@@ -57,7 +57,7 @@
   val empty = Symtab.empty;
   val copy = I;
   val prep_ext = I;
-  val merge = Symtab.merge op =;
+  val merge : T * T -> T = Symtab.merge op =;
   fun print sg _ = ();
 end;