# HG changeset patch
# User wenzelm
# Date 1394099594 -3600
# Node ID 4766342e8376ce9660b0bbdf671b0e55924dd166
# Parent  bb21b380f65d17ca307d82343350ed2c91293eec
clarified check of internal names;

diff -r bb21b380f65d -r 4766342e8376 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Mar 06 10:12:47 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Mar 06 10:53:14 2014 +0100
@@ -422,19 +422,6 @@
 
 
 
-(** 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 *)
@@ -515,7 +502,7 @@
 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) =>
@@ -550,13 +537,12 @@
 
 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;
@@ -1033,8 +1019,10 @@
   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
diff -r bb21b380f65d -r 4766342e8376 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 10:12:47 2014 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 10:53:14 2014 +0100
@@ -257,7 +257,8 @@
                     val _ = report ps (markup_const ctxt) c;
                   in Const (c, T) end)
           | decode ps _ _ (Free (a, T)) =
-              (case (get_free a, get_const a) of
+              (Name.reject_internal (a, ps);
+               case (get_free a, get_const a) of
                 (SOME x, _) => (report ps (markup_free ctxt) x; Free (x, T))
               | (_, (true, c)) => (report ps (markup_const ctxt) c; Const (c, T))
               | (_, (false, c)) =>
diff -r bb21b380f65d -r 4766342e8376 src/Pure/name.ML
--- a/src/Pure/name.ML	Thu Mar 06 10:12:47 2014 +0100
+++ b/src/Pure/name.ML	Thu Mar 06 10:53:14 2014 +0100
@@ -14,9 +14,11 @@
   val internal: string -> string
   val dest_internal: string -> string
   val is_internal: string -> bool
+  val reject_internal: string * Position.T list -> unit
   val skolem: string -> string
   val dest_skolem: string -> string
   val is_skolem: string -> bool
+  val reject_skolem: string * Position.T list -> unit
   val clean_index: string * int -> string * int
   val clean: string -> string
   type context
@@ -61,15 +63,19 @@
 val is_bound = String.isPrefix ":";
 
 
-(* internal names *)
+(* internal names -- NB: internal subsumes skolem *)
 
 val internal = suffix "_";
 val dest_internal = unsuffix "_";
 val is_internal = String.isSuffix "_";
+fun reject_internal (x, ps) =
+  if is_internal x then error ("Bad name: " ^ quote x ^ Position.here_list ps) else ();
 
 val skolem = suffix "__";
 val dest_skolem = unsuffix "__";
 val is_skolem = String.isSuffix "__";
+fun reject_skolem (x, ps) =
+  if is_skolem x then error ("Bad name: " ^ quote x ^ Position.here_list ps) else ();
 
 fun clean_index (x, i) =
   (case try dest_internal x of