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