| changeset 5702 | 77ad51744aee |
| parent 5692 | 2e873c5f0e2c |
| child 6167 | 2f354020efc3 |
--- 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;