# HG changeset patch
# User berghofe
# Date 1098865807 -7200
# Node ID a1547232fedd5a75c9e3023516569d282a418baf
# Parent  a881ad2e9edcf1a9b80b12e2cd156fee2037f242
Added type constraint to make SML/NJ happy.

diff -r a881ad2e9edc -r a1547232fedd 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;