src/Pure/Isar/proof_context.ML

 
 
 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
             (if can Name.dest_skolem x then Markup.skolem else Markup.free)) pos;
           Free (x, infer_type ctxt (x, ty)))