# HG changeset patch
# User wenzelm
# Date 908898772 -7200
# Node ID 77ad51744aee66e5a410763f2145729fc58d4648
# Parent  e57980ec351b3a1955802b2babe2eca2a530e24a
made SML/NJ happy;

diff -r e57980ec351b -r 77ad51744aee src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Tue Oct 20 17:27:00 1998 +0200
+++ b/src/Pure/Syntax/syntax.ML	Tue Oct 20 17:52:52 1998 +0200
@@ -93,7 +93,7 @@
 fun extend_tr'tab tab trfuns =
   generic_extend eq_trfuns Symtab.dest_multi Symtab.make_multi tab (map mk_trfun trfuns);
 
-val merge_tr'tabs = generic_merge eq_trfuns Symtab.dest_multi Symtab.make_multi;
+fun merge_tr'tabs tabs = generic_merge eq_trfuns Symtab.dest_multi Symtab.make_multi tabs;