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