# HG changeset patch
# User wenzelm
# Date 1272571737 -7200
# Node ID 7cb6b40d19b21411d287d9a9d02e88ae23065ced
# Parent  de1862c4a308d7888c38856b539062e3bf654f02
read_const: disallow internal names as usual in visible Isar text;

diff -r de1862c4a308 -r 7cb6b40d19b2 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Apr 29 21:05:54 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu Apr 29 22:08:57 2010 +0200
@@ -505,7 +505,10 @@
 fun read_const_proper ctxt strict = prep_const_proper ctxt strict o token_content;
 
 fun read_const ctxt strict ty text =
-  let val (c, pos) = token_content text in
+  let
+    val (c, pos) = token_content text;
+    val _ = no_skolem false c;
+  in
     (case (lookup_skolem ctxt c, Variable.is_const ctxt c) of
       (SOME x, false) =>
         (Position.report (Markup.name x