# HG changeset patch # User wenzelm # Date 1195652630 -3600 # Node ID 089a82c28a42c8d84d5564edde49daec805f8d7f # Parent 7bd190cac91e0512a7287757a24fa8922ab9e5a4 intern_skolem: disallow qualified names; diff -r 7bd190cac91e -r 089a82c28a42 src/Pure/Isar/proof_context.ML --- 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