changeset 49688 | c517d900805a |
parent 49685 | 4341e4d86872 |
child 50201 | c26369c9eda6 |
--- 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) =>