changeset 55961 | c2d4a3608441 |
parent 55957 | cffb46aea3d1 |
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;