read_const: disallow internal names as usual in visible Isar text;

--- 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