src/Pure/Thy/term_style.ML
changeset 23577 c5b93c69afd3
parent 22846 fb79144af9a3
child 23655 d2d1138e0ddc
--- a/src/Pure/Thy/term_style.ML	Thu Jul 05 00:06:13 2007 +0200
+++ b/src/Pure/Thy/term_style.ML	Thu Jul 05 00:06:14 2007 +0200
@@ -27,7 +27,7 @@
   val empty = Symtab.empty;
   val copy = I;
   val extend = I;
-  fun merge _ tabs = Symtab.merge (eq_snd (op =)) tabs
+  fun merge _ tabs : T = Symtab.merge (eq_snd (op =)) tabs
     handle Symtab.DUPS dups => err_dup_styles dups;
 );