author | wenzelm |
Thu, 06 Mar 2014 20:26:43 +0100 | |
changeset 55961 | c2d4a3608441 |
parent 55960 | beef468837b1 |
child 55962 | fbd0e768bc8f |
--- a/src/Pure/General/name_space.ML Thu Mar 06 19:55:08 2014 +0100 +++ b/src/Pure/General/name_space.ML Thu Mar 06 20:26:43 2014 +0100 @@ -205,7 +205,7 @@ (* completion *) fun completion context space (xname, pos) = - if Context_Position.is_reported_generic context pos then + if Position.is_reported pos then let val x = Name.clean xname; val Name_Space {kind = k, internals, ...} = space;