# HG changeset patch
# User wenzelm
# Date 1247863878 -7200
# Node ID f92df23c33057765b8bac9035f2354350c74a436
# Parent  a6a6e8031c14b7e233375e39d42b0b0c27fa88a8
tuned;

diff -r a6a6e8031c14 -r f92df23c3305 src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Fri Jul 17 21:33:00 2009 +0200
+++ b/src/Pure/type_infer.ML	Fri Jul 17 22:51:18 2009 +0200
@@ -402,7 +402,7 @@
 
     (*convert to preterms*)
     val ts = burrow_types check_typs raw_ts;
-    val (ts', (vps, ps)) =
+    val (ts', _) =
       fold_map (preterm_of const_type is_param o constrain_vars) ts (Vartab.empty, Vartab.empty);
 
     (*do type inference*)