# HG changeset patch
# User obua
# Date 1184147233 -7200
# Node ID d639647a1ffddae31bb49f696f8b31d2b5b6c6c6
# Parent  7272a839ccd93f202bfa5aa14d6dc4fc1bfeadef
fixed for SML/NJ

diff -r 7272a839ccd9 -r d639647a1ffd src/Tools/Compute_Oracle/linker.ML
--- a/src/Tools/Compute_Oracle/linker.ML	Wed Jul 11 11:46:44 2007 +0200
+++ b/src/Tools/Compute_Oracle/linker.ML	Wed Jul 11 11:47:13 2007 +0200
@@ -72,7 +72,7 @@
 
 structure Substtab = TableFun(type key = Type.tyenv val ord = subst_ord);
 
-val substtab_union = Substtab.fold Substtab.update
+fun substtab_union c = Substtab.fold Substtab.update c
 fun substtab_unions [] = Substtab.empty
   | substtab_unions [c] = c
   | substtab_unions (c::cs) = substtab_union c (substtab_unions cs)