src/Pure/Isar/proof_context.ML

 val cert_typ_syntax = cert_typ_mode Type.mode_syntax;
 val cert_typ_abbrev = cert_typ_mode Type.mode_abbrev;
 
 
 
-(** prepare variables **)
-
-(* check Skolem constants *)
-
-fun no_skolem internal x =
-  if Name.is_skolem x then
-    error ("Illegal reference to internal Skolem constant: " ^ quote x)
-  else if not internal andalso Name.is_internal x then
-    error ("Illegal reference to internal variable: " ^ quote x)
-  else x;
-
-
-
 (** prepare terms and propositions **)
 
 (* inferred types of parameters *)
 
 fun infer_type ctxt x =

   prep_const_proper ctxt strict o Symbol_Pos.source_content o Syntax.read_token;
 
 fun read_const ctxt strict ty text =
   let
     val (c, pos) = Symbol_Pos.source_content (Syntax.read_token text);
-    val _ = no_skolem false c;
+    val _ = Name.reject_internal (c, [pos]);
   in
     (case (Variable.lookup_fixed ctxt c, Variable.is_const ctxt c) of
       (SOME x, false) =>
         (Context_Position.report ctxt pos
             (Markup.name x (if Name.is_skolem x then Markup.skolem else Markup.free));

 
 (* skolem variables *)
 
 fun intern_skolem ctxt x =
   let
-    val _ = no_skolem false x;
-    val sko = Variable.lookup_fixed ctxt x;
+    val skolem = Variable.lookup_fixed ctxt x;
     val is_const = can (read_const_proper ctxt false) x orelse Long_Name.is_qualified x;
     val is_declared = is_some (Variable.def_type ctxt false (x, ~1));
   in
     if Variable.is_const ctxt x then NONE
-    else if is_some sko then sko
+    else if is_some skolem then skolem
     else if not is_const orelse is_declared then SOME x
     else NONE
   end;
 
 

 
 fun prep_vars prep_typ internal =
   fold_map (fn (b, raw_T, mx) => fn ctxt =>
     let
       val x = Variable.check_name b;
-      val _ = Symbol_Pos.is_identifier (no_skolem internal x) orelse
-        error ("Illegal variable name: " ^ Binding.print b);
+      val check_name = if internal then Name.reject_skolem else Name.reject_internal;
+      val _ =
+        if can check_name (x, []) andalso Symbol_Pos.is_identifier x then ()
+        else error ("Bad name: " ^ Binding.print b);
 
       fun cond_tvars T =
         if internal then T
         else Type.no_tvars T handle TYPE (msg, _, _) => error msg;
       val opt_T = Option.map (cond_tvars o cert_typ ctxt o prep_typ ctxt) raw_T;