# HG changeset patch
# User wenzelm
# Date 1349275421 -7200
# Node ID c517d900805a28a434401ef4da5fe771b582bf10
# Parent  4b9034f089ebb666686ba3798d39c03da6fe6b7c
tuned;

diff -r 4b9034f089eb -r c517d900805a src/Pure/variable.ML
--- 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) =>