use "fold_map" instead of "fold (fn .. => .. (ts @ [t], ..)) .."
authortraytel
Thu, 02 Dec 2010 21:48:36 +0100
changeset 40938 e258f6817add
parent 40937 e2e0ef28d3f8
child 40939 2c150063cd4d
use "fold_map" instead of "fold (fn .. => .. (ts @ [t], ..)) .."
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) =