src/Pure/variable.ML
changeset 49674 dbadb4d03cbc
parent 47021 f35f654f297d
child 49685 4341e4d86872
     1.1 --- a/src/Pure/variable.ML	Mon Oct 01 12:05:05 2012 +0200
     1.2 +++ b/src/Pure/variable.ML	Mon Oct 01 16:37:22 2012 +0200
     1.3 @@ -214,7 +214,8 @@
     1.4  (* constraints *)
     1.5  
     1.6  fun constrain_tvar (xi, S) =
     1.7 -  if S = dummyS then Vartab.delete_safe xi else Vartab.update (xi, S);
     1.8 +  if S = dummyS orelse Term_Position.is_positionS S
     1.9 +  then Vartab.delete_safe xi else Vartab.update (xi, S);
    1.10  
    1.11  fun declare_constraints t = map_constraints (fn (types, sorts) =>
    1.12    let