author | wenzelm |
Wed, 21 Nov 2007 14:43:50 +0100 | |
changeset 25452 | 089a82c28a42 |
parent 25451 | 7bd190cac91e |
child 25453 | 80557dafd2a0 |
--- a/src/Pure/Isar/proof_context.ML Wed Nov 21 14:18:23 2007 +0100 +++ b/src/Pure/Isar/proof_context.ML Wed Nov 21 14:43:50 2007 +0100 @@ -506,7 +506,7 @@ let val _ = no_skolem false x; val sko = lookup_skolem ctxt x; - val is_const = can (read_const_proper ctxt) x; + val is_const = can (read_const_proper ctxt) x orelse NameSpace.is_qualified x; val is_declared = is_some (def_type (x, ~1)); in if Variable.is_const ctxt x then NONE