# HG changeset patch
# User traytel
# Date 1291322916 -3600
# Node ID e258f6817add851fc3dc7d1fa5e43594e9997aec
# Parent  e2e0ef28d3f8754af2d65dd3b3f9532758955369
use "fold_map" instead of "fold (fn .. => .. (ts @ [t], ..)) .."

diff -r e2e0ef28d3f8 -r e258f6817add src/Tools/subtyping.ML
--- a/src/Tools/subtyping.ML	Fri Dec 03 17:31:27 2010 +0100
+++ b/src/Tools/subtyping.ML	Thu Dec 02 21:48:36 2010 +0100
@@ -685,11 +685,11 @@
                 raise TYPE_INFERENCE_ERROR (err_appl_msg ctxt msg tye' bs t T u U);
           in (tu, V, tye_idx'') end;
 
-    fun infer_single t (ts, tye_idx) = 
+    fun infer_single t tye_idx = 
       let val (t, _, tye_idx') = inf [] t tye_idx;
-      in (ts @ [t], tye_idx') end;
+      in (t, tye_idx') end;
       
-    val (ts', (tye, _)) = (fold infer_single ts ([], (Vartab.empty, idx))
+    val (ts', (tye, _)) = (fold_map infer_single ts (Vartab.empty, idx)
       handle TYPE_INFERENCE_ERROR err =>     
         let
           fun gen_single t (tye_idx, constraints) =