# 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