tuned;

--- a/src/Pure/variable.ML	Wed Oct 03 16:42:36 2012 +0200
+++ b/src/Pure/variable.ML	Wed Oct 03 16:43:41 2012 +0200
@@ -214,7 +214,7 @@
 (* constraints *)
 
 fun constrain_tvar (xi, raw_S) =
-  let val (_, S) = Term_Position.decode_positionS raw_S
+  let val S = #2 (Term_Position.decode_positionS raw_S)
   in if S = dummyS then Vartab.delete_safe xi else Vartab.update (xi, S) end;
 
 fun declare_constraints t = map_constraints (fn (types, sorts) =>