src/HOL/Tools/typedef_package.ML
changeset 15265 a1547232fedd
parent 15259 6aa593317905
child 15457 1fbd4aba46e3
--- 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;