src/Pure/variable.ML

--- a/src/Pure/variable.ML	Mon Oct 01 12:05:05 2012 +0200
+++ b/src/Pure/variable.ML	Mon Oct 01 16:37:22 2012 +0200
@@ -214,7 +214,8 @@
 (* constraints *)
 
 fun constrain_tvar (xi, S) =
-  if S = dummyS then Vartab.delete_safe xi else Vartab.update (xi, S);
+  if S = dummyS orelse Term_Position.is_positionS S
+  then Vartab.delete_safe xi else Vartab.update (xi, S);
 
 fun declare_constraints t = map_constraints (fn (types, sorts) =>
   let