1.1 --- a/src/Doc/antiquote_setup.ML	Mon Nov 26 21:10:42 2012 +0100
     1.2 +++ b/src/Doc/antiquote_setup.ML	Mon Nov 26 21:46:04 2012 +0100
     1.3 @@ -80,7 +80,7 @@
     1.4          if txt2 = "" then txt1
     1.5          else if kind = "type" then txt1 ^ " = " ^ txt2
     1.6          else if kind = "exception" then txt1 ^ " of " ^ txt2
     1.7 -        else if Lexicon.is_identifier (Long_Name.base_name (ml_name txt1))
     1.8 +        else if Symbol_Pos.is_identifier (Long_Name.base_name (ml_name txt1))
     1.9          then txt1 ^ ": " ^ txt2
    1.10          else txt1 ^ " : " ^ txt2;
    1.11        val txt' = if kind = "" then txt else kind ^ " " ^ txt;

     2.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Mon Nov 26 21:10:42 2012 +0100
     2.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Mon Nov 26 21:46:04 2012 +0100
     2.3 @@ -126,7 +126,7 @@
     2.4  
     2.5  val unyxml = XML.content_of o YXML.parse_body
     2.6  
     2.7 -val is_long_identifier = forall Lexicon.is_identifier o Long_Name.explode
     2.8 +val is_long_identifier = forall Symbol_Pos.is_identifier o Long_Name.explode
     2.9  fun maybe_quote y =
    2.10    let val s = unyxml y in
    2.11      y |> ((not (is_long_identifier (perhaps (try (unprefix "'")) s)) andalso

     3.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Mon Nov 26 21:10:42 2012 +0100
     3.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Mon Nov 26 21:46:04 2012 +0100
     3.3 @@ -232,7 +232,7 @@
     3.4        let val s' = Long_Name.base_name s in
     3.5          space_implode "_"
     3.6            (filter_out (equal "") (map name_of_typ Ts) @
     3.7 -            [if Lexicon.is_identifier s' then s' else "x"])
     3.8 +            [if Symbol_Pos.is_identifier s' then s' else "x"])
     3.9        end
    3.10    | name_of_typ _ = "";
    3.11  

     4.1 --- a/src/HOL/Tools/Datatype/datatype_prop.ML	Mon Nov 26 21:10:42 2012 +0100
     4.2 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Mon Nov 26 21:46:04 2012 +0100
     4.3 @@ -46,7 +46,7 @@
     4.4      fun type_name (TFree (name, _)) = unprefix "'" name
     4.5        | type_name (Type (name, _)) =
     4.6            let val name' = Long_Name.base_name name
     4.7 -          in if Lexicon.is_identifier name' then name' else "x" end;
     4.8 +          in if Symbol_Pos.is_identifier name' then name' else "x" end;
     4.9    in indexify_names (map type_name Ts) end;
    4.10  
    4.11  

     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Nov 26 21:10:42 2012 +0100
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Nov 26 21:46:04 2012 +0100
     5.3 @@ -61,7 +61,7 @@
     5.4  
     5.5  fun needs_quoting reserved s =
     5.6    Symtab.defined reserved s orelse
     5.7 -  exists (not o Lexicon.is_identifier) (Long_Name.explode s)
     5.8 +  exists (not o Symbol_Pos.is_identifier) (Long_Name.explode s)
     5.9  
    5.10  fun make_name reserved multi j name =
    5.11    (name |> needs_quoting reserved name ? quote) ^

     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Nov 26 21:10:42 2012 +0100
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Nov 26 21:46:04 2012 +0100
     6.3 @@ -224,7 +224,7 @@
     6.4      "using " ^ space_implode " " (map string_for_label ls) ^ " "
     6.5  
     6.6  fun command_call name [] =
     6.7 -    name |> not (Lexicon.is_identifier name) ? enclose "(" ")"
     6.8 +    name |> not (Symbol_Pos.is_identifier name) ? enclose "(" ")"
     6.9    | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
    6.10  
    6.11  fun reconstructor_command reconstr i n used_chaineds num_chained (ls, ss) =

     7.1 --- a/src/HOL/Tools/choice_specification.ML	Mon Nov 26 21:10:42 2012 +0100
     7.2 +++ b/src/HOL/Tools/choice_specification.ML	Mon Nov 26 21:46:04 2012 +0100
     7.3 @@ -166,7 +166,7 @@
     7.4              let
     7.5                  val T = type_of c
     7.6                  val cname = Long_Name.base_name (fst (dest_Const c))
     7.7 -                val vname = if Lexicon.is_identifier cname
     7.8 +                val vname = if Symbol_Pos.is_identifier cname
     7.9                              then cname
    7.10                              else "x"
    7.11              in

     8.1 --- a/src/Pure/General/binding.ML	Mon Nov 26 21:10:42 2012 +0100
     8.2 +++ b/src/Pure/General/binding.ML	Mon Nov 26 21:46:04 2012 +0100
     8.3 @@ -136,7 +136,7 @@
     8.4  fun bad binding = "Bad name binding: " ^ print binding ^ Position.here (pos_of binding);
     8.5  
     8.6  fun check binding =
     8.7 -  if Symbol.is_ident (Symbol.explode (name_of binding)) then ()
     8.8 +  if Symbol_Pos.is_identifier (name_of binding) then ()
     8.9    else legacy_feature (bad binding);
    8.10  
    8.11  end;

     9.1 --- a/src/Pure/General/symbol.ML	Mon Nov 26 21:10:42 2012 +0100
     9.2 +++ b/src/Pure/General/symbol.ML	Mon Nov 26 21:46:04 2012 +0100
     9.3 @@ -53,7 +53,6 @@
     9.4    val is_block_ctrl: symbol -> bool
     9.5    val is_quasi_letter: symbol -> bool
     9.6    val is_letdig: symbol -> bool
     9.7 -  val is_ident: symbol list -> bool
     9.8    val beginning: int -> symbol list -> string
     9.9    val source: (string, 'a) Source.source -> (symbol, (string, 'a) Source.source) Source.source
    9.10    val explode: string -> symbol list
    9.11 @@ -512,12 +511,6 @@
    9.12    |> implode;
    9.13  
    9.14  
    9.15 -(* identifiers *)
    9.16 -
    9.17 -fun is_ident [] = false
    9.18 -  | is_ident (c :: cs) = is_letter c andalso forall is_letdig cs;
    9.19 -
    9.20 -
    9.21  (* bump string -- treat as base 26 or base 1 numbers *)
    9.22  
    9.23  fun symbolic_end (_ :: "\\<^isub>" :: _) = true

    10.1 --- a/src/Pure/General/symbol_pos.ML	Mon Nov 26 21:10:42 2012 +0100
    10.2 +++ b/src/Pure/General/symbol_pos.ML	Mon Nov 26 21:46:04 2012 +0100
    10.3 @@ -37,6 +37,9 @@
    10.4    val range: T list -> Position.range
    10.5    val implode_range: Position.T -> Position.T -> T list -> text * Position.range
    10.6    val explode: text * Position.T -> T list
    10.7 +  val scan_ident: T list -> T list * T list
    10.8 +  val is_ident: T list -> bool
    10.9 +  val is_identifier: string -> bool
   10.10  end;
   10.11  
   10.12  structure Symbol_Pos: SYMBOL_POS =
   10.13 @@ -208,6 +211,18 @@
   10.14          (Symbol.explode str) ([], Position.reset_range pos);
   10.15    in fold (fn (s, p) => if s = Symbol.DEL then I else cons (s, p)) res [] end;
   10.16  
   10.17 +
   10.18 +(* identifiers *)
   10.19 +
   10.20 +val scan_ident =
   10.21 +  Scan.one (Symbol.is_letter o symbol) ::: Scan.many (Symbol.is_letdig o symbol);
   10.22 +
   10.23 +fun is_ident [] = false
   10.24 +  | is_ident (s :: ss) = Symbol.is_letter (symbol s) andalso forall (Symbol.is_letdig o symbol) ss;
   10.25 +
   10.26 +fun is_identifier s =
   10.27 +  Symbol.is_ascii_identifier s orelse is_ident (explode (s, Position.none));
   10.28 +
   10.29  end;
   10.30  
   10.31  structure Basic_Symbol_Pos =   (*not open by default*)

    11.1 --- a/src/Pure/Isar/proof_context.ML	Mon Nov 26 21:10:42 2012 +0100
    11.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Nov 26 21:46:04 2012 +0100
    11.3 @@ -974,7 +974,7 @@
    11.4    fold_map (fn (b, raw_T, mx) => fn ctxt =>
    11.5      let
    11.6        val x = Variable.check_name b;
    11.7 -      val _ = Lexicon.is_identifier (no_skolem internal x) orelse
    11.8 +      val _ = Symbol_Pos.is_identifier (no_skolem internal x) orelse
    11.9          error ("Illegal variable name: " ^ Binding.print b);
   11.10  
   11.11        fun cond_tvars T =

    12.1 --- a/src/Pure/Isar/token.ML	Mon Nov 26 21:10:42 2012 +0100
    12.2 +++ b/src/Pure/Isar/token.ML	Mon Nov 26 21:46:04 2012 +0100
    12.3 @@ -311,7 +311,7 @@
    12.4  fun ident_or_symbolic "begin" = false
    12.5    | ident_or_symbolic ":" = true
    12.6    | ident_or_symbolic "::" = true
    12.7 -  | ident_or_symbolic s = Lexicon.is_identifier s orelse is_symid s;
    12.8 +  | ident_or_symbolic s = Symbol_Pos.is_identifier s orelse is_symid s;
    12.9  
   12.10  
   12.11  (* scan verbatim text *)

    13.1 --- a/src/Pure/Syntax/lexicon.ML	Mon Nov 26 21:10:42 2012 +0100
    13.2 +++ b/src/Pure/Syntax/lexicon.ML	Mon Nov 26 21:46:04 2012 +0100
    13.3 @@ -12,9 +12,6 @@
    13.4      val free: string -> term
    13.5      val var: indexname -> term
    13.6    end
    13.7 -  val is_identifier: string -> bool
    13.8 -  val is_xid: string -> bool
    13.9 -  val is_tid: string -> bool
   13.10    val scan_id: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
   13.11    val scan_longid: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
   13.12    val scan_tid: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
   13.13 @@ -25,6 +22,7 @@
   13.14    val scan_bin: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
   13.15    val scan_var: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
   13.16    val scan_tvar: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
   13.17 +  val is_tid: string -> bool
   13.18    datatype token_kind =
   13.19      Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy |
   13.20      NumSy | FloatSy | XNumSy | StrSy | Space | Comment | EOF
   13.21 @@ -90,32 +88,13 @@
   13.22  
   13.23  
   13.24  
   13.25 -(** is_identifier etc. **)
   13.26 -
   13.27 -val is_identifier = Symbol.is_ident o Symbol.explode;
   13.28 -
   13.29 -fun is_xid s =
   13.30 -  (case Symbol.explode s of
   13.31 -    "_" :: cs => Symbol.is_ident cs
   13.32 -  | cs => Symbol.is_ident cs);
   13.33 -
   13.34 -fun is_tid s =
   13.35 -  (case Symbol.explode s of
   13.36 -    "'" :: cs => Symbol.is_ident cs
   13.37 -  | _ => false);
   13.38 -
   13.39 -
   13.40 -
   13.41  (** basic scanners **)
   13.42  
   13.43  open Basic_Symbol_Pos;
   13.44  
   13.45  fun !!! msg = Symbol_Pos.!!! (fn () => "Inner lexical error: " ^ msg);
   13.46  
   13.47 -val scan_id =
   13.48 -  Scan.one (Symbol.is_letter o Symbol_Pos.symbol) :::
   13.49 -  Scan.many (Symbol.is_letdig o Symbol_Pos.symbol);
   13.50 -
   13.51 +val scan_id = Symbol_Pos.scan_ident;
   13.52  val scan_longid = scan_id @@@ (Scan.repeat1 ($$$ "." @@@ scan_id) >> flat);
   13.53  val scan_tid = $$$ "'" @@@ scan_id;
   13.54  
   13.55 @@ -130,6 +109,11 @@
   13.56  val scan_var = $$$ "?" @@@ scan_id_nat;
   13.57  val scan_tvar = $$$ "?" @@@ $$$ "'" @@@ scan_id_nat;
   13.58  
   13.59 +fun is_tid s =
   13.60 +  (case try (unprefix "'") s of
   13.61 +    SOME s' => Symbol_Pos.is_identifier s'
   13.62 +  | NONE => false);
   13.63 +
   13.64  
   13.65  
   13.66  (** datatype token **)
   13.67 @@ -315,7 +299,8 @@
   13.68            if Symbol.is_digit c then chop_idx cs (c :: ds)
   13.69            else idxname (c :: cs) ds;
   13.70  
   13.71 -    val scan = (scan_id >> map Symbol_Pos.symbol) --
   13.72 +    val scan =
   13.73 +      (scan_id >> map Symbol_Pos.symbol) --
   13.74        Scan.optional ($$$ "." |-- scan_nat >> (nat 0 o map Symbol_Pos.symbol)) ~1;
   13.75    in
   13.76      scan >>

    14.1 --- a/src/Pure/tactic.ML	Mon Nov 26 21:10:42 2012 +0100
    14.2 +++ b/src/Pure/tactic.ML	Mon Nov 26 21:46:04 2012 +0100
    14.3 @@ -306,7 +306,7 @@
    14.4  
    14.5  (*Renaming of parameters in a subgoal*)
    14.6  fun rename_tac xs i =
    14.7 -  case Library.find_first (not o Lexicon.is_identifier) xs of
    14.8 +  case Library.find_first (not o Symbol_Pos.is_identifier) xs of
    14.9        SOME x => error ("Not an identifier: " ^ x)
   14.10      | NONE => PRIMITIVE (Thm.rename_params_rule (xs, i));
   14.11  

    15.1 --- a/src/ZF/Tools/datatype_package.ML	Mon Nov 26 21:10:42 2012 +0100
    15.2 +++ b/src/ZF/Tools/datatype_package.ML	Mon Nov 26 21:46:04 2012 +0100
    15.3 @@ -130,7 +130,7 @@
    15.4  
    15.5    (*The function variable for a single constructor*)
    15.6    fun add_case ((_, T, _), name, args, _) (opno, cases) =
    15.7 -    if Lexicon.is_identifier name then
    15.8 +    if Symbol_Pos.is_identifier name then
    15.9        (opno, (Free (case_varname ^ "_" ^ name, T), args) :: cases)
   15.10      else
   15.11        (opno + 1, (Free (case_varname ^ "_op_" ^ string_of_int opno, T), args)

    16.1 --- a/src/ZF/Tools/inductive_package.ML	Mon Nov 26 21:10:42 2012 +0100
    16.2 +++ b/src/ZF/Tools/inductive_package.ML	Mon Nov 26 21:46:04 2012 +0100
    16.3 @@ -78,7 +78,7 @@
    16.4    and (Const(_,recT),rec_params) = strip_comb (hd rec_tms);
    16.5  
    16.6    val rec_base_names = map Long_Name.base_name rec_names;
    16.7 -  val dummy = assert_all Lexicon.is_identifier rec_base_names
    16.8 +  val dummy = assert_all Symbol_Pos.is_identifier rec_base_names
    16.9      (fn a => "Base name of recursive set not an identifier: " ^ a);
   16.10  
   16.11    local (*Checking the introduction rules*)