tuned;

--- 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*)