discontinued special treatment of structure Lexicon;
authorwenzelm
Fri Apr 08 16:34:14 2011 +0200 (2011-04-08)
changeset 42290b1f544c84040
parent 42289 dafae095d733
child 42292 b3196458428b
discontinued special treatment of structure Lexicon;
NEWS
doc-src/antiquote_setup.ML
src/HOL/HOLCF/Tools/Domain/domain_constructors.ML
src/HOL/HOLCF/Tools/cont_consts.ML
src/HOL/HOLCF/ex/Pattern_Match.thy
src/HOL/Import/proof_kernel.ML
src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
src/HOL/Tools/Datatype/datatype_aux.ML
src/HOL/Tools/Datatype/datatype_case.ML
src/HOL/Tools/Datatype/datatype_data.ML
src/HOL/Tools/Datatype/datatype_prop.ML
src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
src/HOL/Tools/choice_specification.ML
src/HOL/Tools/float_syntax.ML
src/HOL/Tools/numeral_syntax.ML
src/HOL/Tools/record.ML
src/HOL/Tools/string_syntax.ML
src/HOL/Tools/typedef.ML
src/HOL/ex/Binary.thy
src/HOL/ex/Numeral.thy
src/Pure/Isar/expression.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/token.ML
src/Pure/ML/ml_antiquote.ML
src/Pure/ML/ml_syntax.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/Syntax/lexicon.ML
src/Pure/Syntax/local_syntax.ML
src/Pure/Syntax/syntax.ML
src/Pure/Syntax/syntax_phases.ML
src/Pure/Thy/latex.ML
src/Pure/Thy/thy_syntax.ML
src/Pure/consts.ML
src/Pure/pure_thy.ML
src/Pure/sign.ML
src/Pure/tactic.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/inductive_package.ML
src/ZF/Tools/numeral_syntax.ML
     1.1 --- a/NEWS	Fri Apr 08 15:48:14 2011 +0200
     1.2 +++ b/NEWS	Fri Apr 08 16:34:14 2011 +0200
     1.3 @@ -93,10 +93,11 @@
     1.4  be disabled via the configuration option Syntax.positions, which is
     1.5  called "syntax_positions" in Isar attribute syntax.
     1.6  
     1.7 -* Discontinued special treatment of various ML structures of inner
     1.8 -syntax, such as structure Ast: no pervasive content, no inclusion in
     1.9 -structure Syntax.  INCOMPATIBILITY, refer to qualified names like
    1.10 -Ast.Constant etc.
    1.11 +* Discontinued special status of various ML structures that contribute
    1.12 +to structure Syntax (Ast, Lexicon, Mixfix, Parser, Printer etc.): less
    1.13 +pervasive content, no inclusion in structure Syntax.  INCOMPATIBILITY,
    1.14 +refer directly to Ast.Constant, Lexicon.is_identifier,
    1.15 +Syntax_Trans.mk_binder_tr etc.
    1.16  
    1.17  * Typed print translation: discontinued show_sorts argument, which is
    1.18  already available via context of "advanced" translation.
     2.1 --- a/doc-src/antiquote_setup.ML	Fri Apr 08 15:48:14 2011 +0200
     2.2 +++ b/doc-src/antiquote_setup.ML	Fri Apr 08 16:34:14 2011 +0200
     2.3 @@ -71,7 +71,8 @@
     2.4          if txt2 = "" then txt1
     2.5          else if kind = "type" then txt1 ^ " = " ^ txt2
     2.6          else if kind = "exception" then txt1 ^ " of " ^ txt2
     2.7 -        else if Syntax.is_identifier (Long_Name.base_name (ml_name txt1)) then txt1 ^ ": " ^ txt2
     2.8 +        else if Lexicon.is_identifier (Long_Name.base_name (ml_name txt1))
     2.9 +        then txt1 ^ ": " ^ txt2
    2.10          else txt1 ^ " : " ^ txt2;
    2.11        val txt' = if kind = "" then txt else kind ^ " " ^ txt;
    2.12        val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none (ml (txt1, txt2));  (* ML_Lex.read (!?) *)
     3.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Fri Apr 08 15:48:14 2011 +0200
     3.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Fri Apr 08 16:34:14 2011 +0200
     3.3 @@ -442,7 +442,7 @@
     3.4      (* define syntax for case combinator *)
     3.5      (* TODO: re-implement case syntax using a parse translation *)
     3.6      local
     3.7 -      fun syntax c = Syntax.mark_const (fst (dest_Const c))
     3.8 +      fun syntax c = Lexicon.mark_const (fst (dest_Const c))
     3.9        fun xconst c = Long_Name.base_name (fst (dest_Const c))
    3.10        fun c_ast authentic con = Ast.Constant (if authentic then syntax con else xconst con)
    3.11        fun showint n = string_of_int (n+1)
     4.1 --- a/src/HOL/HOLCF/Tools/cont_consts.ML	Fri Apr 08 15:48:14 2011 +0200
     4.2 +++ b/src/HOL/HOLCF/Tools/cont_consts.ML	Fri Apr 08 16:34:14 2011 +0200
     4.3 @@ -47,7 +47,7 @@
     4.4  *)
     4.5  fun transform thy (c, T, mx) =
     4.6    let
     4.7 -    fun syntax b = Syntax.mark_const (Sign.full_bname thy b)
     4.8 +    fun syntax b = Lexicon.mark_const (Sign.full_bname thy b)
     4.9      val c1 = Binding.name_of c
    4.10      val c2 = c1 ^ "_cont_syntax"
    4.11      val n = Mixfix.mixfix_args mx
     5.1 --- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Fri Apr 08 15:48:14 2011 +0200
     5.2 +++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Fri Apr 08 16:34:14 2011 +0200
     5.3 @@ -497,7 +497,7 @@
     5.4  
     5.5      (* syntax translations for pattern combinators *)
     5.6      local
     5.7 -      fun syntax c = Syntax.mark_const (fst (dest_Const c));
     5.8 +      fun syntax c = Lexicon.mark_const (fst (dest_Const c));
     5.9        fun app s (l, r) = Ast.mk_appl (Ast.Constant s) [l, r];
    5.10        val capp = app @{const_syntax Rep_cfun};
    5.11        val capps = Library.foldl capp
     6.1 --- a/src/HOL/Import/proof_kernel.ML	Fri Apr 08 15:48:14 2011 +0200
     6.2 +++ b/src/HOL/Import/proof_kernel.ML	Fri Apr 08 16:34:14 2011 +0200
     6.3 @@ -181,11 +181,11 @@
     6.4  val string_of_mixfix = Pretty.string_of o Mixfix.pretty_mixfix;
     6.5  
     6.6  fun mk_syn thy c =
     6.7 -  if Syntax.is_identifier c andalso not (Syntax.is_keyword (Sign.syn_of thy) c) then NoSyn
     6.8 +  if Lexicon.is_identifier c andalso not (Syntax.is_keyword (Sign.syn_of thy) c) then NoSyn
     6.9    else Delimfix (Syntax_Ext.escape c)
    6.10  
    6.11  fun quotename c =
    6.12 -  if Syntax.is_identifier c andalso not (Keyword.is_keyword c) then c else quote c
    6.13 +  if Lexicon.is_identifier c andalso not (Keyword.is_keyword c) then c else quote c
    6.14  
    6.15  fun simple_smart_string_of_cterm ctxt0 ct =
    6.16      let
    6.17 @@ -454,7 +454,7 @@
    6.18  val protected_varnames = Unsynchronized.ref (Symtab.empty:string Symtab.table)
    6.19  val invented_isavar = Unsynchronized.ref 0
    6.20  
    6.21 -fun innocent_varname s = Syntax.is_identifier s andalso not (String.isPrefix "u_" s)
    6.22 +fun innocent_varname s = Lexicon.is_identifier s andalso not (String.isPrefix "u_" s)
    6.23  
    6.24  fun valid_boundvarname s =
    6.25    can (fn () => Syntax.read_term_global @{theory Main} ("SOME "^s^". True")) ();
     7.1 --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Fri Apr 08 15:48:14 2011 +0200
     7.2 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Fri Apr 08 16:34:14 2011 +0200
     7.3 @@ -32,7 +32,7 @@
     7.4  let
     7.5    fun cart t u = Syntax.const @{type_syntax cart} $ t $ u;
     7.6    fun finite_cart_tr [t, u as Free (x, _)] =
     7.7 -        if Syntax.is_tid x then
     7.8 +        if Lexicon.is_tid x then
     7.9            cart t (Syntax.const @{syntax_const "_ofsort"} $ u $ Syntax.const @{class_syntax finite})
    7.10          else cart t u
    7.11      | finite_cart_tr [t, u] = cart t u
     8.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Apr 08 15:48:14 2011 +0200
     8.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Apr 08 16:34:14 2011 +0200
     8.3 @@ -232,7 +232,7 @@
     8.4  fun name_of_typ (Type (s, Ts)) =
     8.5        let val s' = Long_Name.base_name s
     8.6        in space_implode "_" (filter_out (equal "") (map name_of_typ Ts) @
     8.7 -        [if Syntax.is_identifier s' then s' else "x"])
     8.8 +        [if Lexicon.is_identifier s' then s' else "x"])
     8.9        end
    8.10    | name_of_typ _ = "";
    8.11  
     9.1 --- a/src/HOL/Tools/Datatype/datatype_case.ML	Fri Apr 08 15:48:14 2011 +0200
     9.2 +++ b/src/HOL/Tools/Datatype/datatype_case.ML	Fri Apr 08 16:34:14 2011 +0200
     9.3 @@ -418,7 +418,7 @@
     9.4    | _ => NONE);
     9.5  
     9.6  val dest_case = gen_dest_case (try (dest_Const #> fst)) fastype_of;
     9.7 -val dest_case' = gen_dest_case (try (dest_Const #> fst #> Syntax.unmark_const)) (K dummyT);
     9.8 +val dest_case' = gen_dest_case (try (dest_Const #> fst #> Lexicon.unmark_const)) (K dummyT);
     9.9  
    9.10  
    9.11  (* destruct nested patterns *)
    9.12 @@ -455,7 +455,7 @@
    9.13          Syntax.const @{syntax_const "_case1"} $
    9.14            map_aterms
    9.15              (fn Free p => Syntax_Trans.mark_boundT p
    9.16 -              | Const (s, _) => Syntax.const (Syntax.mark_const s)
    9.17 +              | Const (s, _) => Syntax.const (Lexicon.mark_const s)
    9.18                | t => t) pat $
    9.19            map_aterms
    9.20              (fn x as Free (s, T) =>
    10.1 --- a/src/HOL/Tools/Datatype/datatype_data.ML	Fri Apr 08 15:48:14 2011 +0200
    10.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML	Fri Apr 08 16:34:14 2011 +0200
    10.3 @@ -224,7 +224,7 @@
    10.4  fun add_case_tr' case_names thy =
    10.5    Sign.add_advanced_trfuns ([], [],
    10.6      map (fn case_name =>
    10.7 -      let val case_name' = Syntax.mark_const case_name
    10.8 +      let val case_name' = Lexicon.mark_const case_name
    10.9        in (case_name', Datatype_Case.case_tr' info_of_case case_name')
   10.10        end) case_names, []) thy;
   10.11  
    11.1 --- a/src/HOL/Tools/Datatype/datatype_prop.ML	Fri Apr 08 15:48:14 2011 +0200
    11.2 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Fri Apr 08 16:34:14 2011 +0200
    11.3 @@ -49,7 +49,7 @@
    11.4      fun type_name (TFree (name, _)) = unprefix "'" name
    11.5        | type_name (Type (name, _)) =
    11.6            let val name' = Long_Name.base_name name
    11.7 -          in if Syntax.is_identifier name' then name' else "x" end;
    11.8 +          in if Lexicon.is_identifier name' then name' else "x" end;
    11.9    in indexify_names (map type_name Ts) end;
   11.10  
   11.11  
    12.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Fri Apr 08 15:48:14 2011 +0200
    12.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Fri Apr 08 16:34:14 2011 +0200
    12.3 @@ -99,7 +99,7 @@
    12.4  
    12.5  fun needs_quoting reserved s =
    12.6    Symtab.defined reserved s orelse
    12.7 -  exists (not o Syntax.is_identifier) (Long_Name.explode s)
    12.8 +  exists (not o Lexicon.is_identifier) (Long_Name.explode s)
    12.9  
   12.10  fun make_name reserved multi j name =
   12.11    (name |> needs_quoting reserved name ? quote) ^
    13.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Apr 08 15:48:14 2011 +0200
    13.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Apr 08 16:34:14 2011 +0200
    13.3 @@ -72,7 +72,7 @@
    13.4  
    13.5  val unyxml = XML.content_of o YXML.parse_body
    13.6  
    13.7 -val is_long_identifier = forall Syntax.is_identifier o space_explode "."
    13.8 +val is_long_identifier = forall Lexicon.is_identifier o space_explode "."
    13.9  fun maybe_quote y =
   13.10    let val s = unyxml y in
   13.11      y |> ((not (is_long_identifier (perhaps (try (unprefix "'")) s)) andalso
    14.1 --- a/src/HOL/Tools/choice_specification.ML	Fri Apr 08 15:48:14 2011 +0200
    14.2 +++ b/src/HOL/Tools/choice_specification.ML	Fri Apr 08 16:34:14 2011 +0200
    14.3 @@ -160,7 +160,7 @@
    14.4              let
    14.5                  val T = type_of c
    14.6                  val cname = Long_Name.base_name (fst (dest_Const c))
    14.7 -                val vname = if Syntax.is_identifier cname
    14.8 +                val vname = if Lexicon.is_identifier cname
    14.9                              then cname
   14.10                              else "x"
   14.11              in
    15.1 --- a/src/HOL/Tools/float_syntax.ML	Fri Apr 08 15:48:14 2011 +0200
    15.2 +++ b/src/HOL/Tools/float_syntax.ML	Fri Apr 08 16:34:14 2011 +0200
    15.3 @@ -27,7 +27,7 @@
    15.4  
    15.5  fun mk_frac str =
    15.6    let
    15.7 -    val {mant = i, exp = n} = Syntax.read_float str;
    15.8 +    val {mant = i, exp = n} = Lexicon.read_float str;
    15.9      val exp = Syntax.const @{const_syntax Power.power};
   15.10      val ten = mk_number 10;
   15.11      val exp10 = if n = 1 then ten else exp $ ten $ mk_number n;
    16.1 --- a/src/HOL/Tools/numeral_syntax.ML	Fri Apr 08 15:48:14 2011 +0200
    16.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Fri Apr 08 16:34:14 2011 +0200
    16.3 @@ -22,7 +22,7 @@
    16.4      fun mk 0 = Syntax.const @{const_name Int.Pls}
    16.5        | mk ~1 = Syntax.const @{const_name Int.Min}
    16.6        | mk i = let val (q, r) = Integer.div_mod i 2 in bit r (mk q) end;
    16.7 -  in mk (#value (Syntax.read_xnum num)) end;
    16.8 +  in mk (#value (Lexicon.read_xnum num)) end;
    16.9  
   16.10  in
   16.11  
    17.1 --- a/src/HOL/Tools/record.ML	Fri Apr 08 15:48:14 2011 +0200
    17.2 +++ b/src/HOL/Tools/record.ML	Fri Apr 08 16:34:14 2011 +0200
    17.3 @@ -715,7 +715,7 @@
    17.4                      val more' = mk_ext rest;
    17.5                    in
    17.6                      list_comb
    17.7 -                      (Syntax.const (Syntax.mark_type (suffix ext_typeN ext)), alphas' @ [more'])
    17.8 +                      (Syntax.const (Lexicon.mark_type (suffix ext_typeN ext)), alphas' @ [more'])
    17.9                    end
   17.10                | NONE => err ("no fields defined for " ^ ext))
   17.11            | NONE => err (name ^ " is no proper field"))
   17.12 @@ -760,7 +760,7 @@
   17.13                    let
   17.14                      val (args, rest) = split_args (map fst (fst (split_last fields))) fargs;
   17.15                      val more' = mk_ext rest;
   17.16 -                  in list_comb (Syntax.const (Syntax.mark_const (ext ^ extN)), args @ [more']) end
   17.17 +                  in list_comb (Syntax.const (Lexicon.mark_const (ext ^ extN)), args @ [more']) end
   17.18                | NONE => err ("no fields defined for " ^ ext))
   17.19            | NONE => err (name ^ " is no proper field"))
   17.20        | mk_ext [] = more;
   17.21 @@ -889,14 +889,14 @@
   17.22  
   17.23  fun record_ext_type_tr' name =
   17.24    let
   17.25 -    val ext_type_name = Syntax.mark_type (suffix ext_typeN name);
   17.26 +    val ext_type_name = Lexicon.mark_type (suffix ext_typeN name);
   17.27      fun tr' ctxt ts =
   17.28        record_type_tr' ctxt (list_comb (Syntax.const ext_type_name, ts));
   17.29    in (ext_type_name, tr') end;
   17.30  
   17.31  fun record_ext_type_abbr_tr' abbr alphas zeta last_ext schemeT name =
   17.32    let
   17.33 -    val ext_type_name = Syntax.mark_type (suffix ext_typeN name);
   17.34 +    val ext_type_name = Lexicon.mark_type (suffix ext_typeN name);
   17.35      fun tr' ctxt ts =
   17.36        record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt
   17.37          (list_comb (Syntax.const ext_type_name, ts));
   17.38 @@ -919,7 +919,7 @@
   17.39      fun strip_fields t =
   17.40        (case strip_comb t of
   17.41          (Const (ext, _), args as (_ :: _)) =>
   17.42 -          (case try (Syntax.unmark_const o unsuffix extN) ext of
   17.43 +          (case try (Lexicon.unmark_const o unsuffix extN) ext of
   17.44              SOME ext' =>
   17.45                (case get_extfields thy ext' of
   17.46                  SOME fields =>
   17.47 @@ -946,7 +946,7 @@
   17.48  
   17.49  fun record_ext_tr' name =
   17.50    let
   17.51 -    val ext_name = Syntax.mark_const (name ^ extN);
   17.52 +    val ext_name = Lexicon.mark_const (name ^ extN);
   17.53      fun tr' ctxt ts = record_tr' ctxt (list_comb (Syntax.const ext_name, ts));
   17.54    in (ext_name, tr') end;
   17.55  
   17.56 @@ -956,7 +956,7 @@
   17.57  local
   17.58  
   17.59  fun dest_update ctxt c =
   17.60 -  (case try Syntax.unmark_const c of
   17.61 +  (case try Lexicon.unmark_const c of
   17.62      SOME d => try (unsuffix updateN) (Consts.extern (ProofContext.consts_of ctxt) d)
   17.63    | NONE => NONE);
   17.64  
   17.65 @@ -982,7 +982,7 @@
   17.66  
   17.67  fun field_update_tr' name =
   17.68    let
   17.69 -    val update_name = Syntax.mark_const (name ^ updateN);
   17.70 +    val update_name = Lexicon.mark_const (name ^ updateN);
   17.71      fun tr' ctxt [t, u] = record_update_tr' ctxt (Syntax.const update_name $ t $ u)
   17.72        | tr' _ _ = raise Match;
   17.73    in (update_name, tr') end;
    18.1 --- a/src/HOL/Tools/string_syntax.ML	Fri Apr 08 15:48:14 2011 +0200
    18.2 +++ b/src/HOL/Tools/string_syntax.ML	Fri Apr 08 16:34:14 2011 +0200
    18.3 @@ -16,11 +16,11 @@
    18.4  (* nibble *)
    18.5  
    18.6  val mk_nib =
    18.7 -  Ast.Constant o Syntax.mark_const o
    18.8 +  Ast.Constant o Lexicon.mark_const o
    18.9      fst o Term.dest_Const o HOLogic.mk_nibble;
   18.10  
   18.11  fun dest_nib (Ast.Constant s) =
   18.12 -  (case try Syntax.unmark_const s of
   18.13 +  (case try Lexicon.unmark_const s of
   18.14      NONE => raise Match
   18.15    | SOME c => (HOLogic.dest_nibble (Const (c, HOLogic.nibbleT)) handle TERM _ => raise Match));
   18.16  
   18.17 @@ -44,11 +44,12 @@
   18.18    | dest_char _ = raise Match;
   18.19  
   18.20  fun syntax_string cs =
   18.21 -  Ast.Appl [Ast.Constant @{syntax_const "_inner_string"}, Ast.Variable (Syntax.implode_xstr cs)];
   18.22 +  Ast.Appl [Ast.Constant @{syntax_const "_inner_string"},
   18.23 +    Ast.Variable (Lexicon.implode_xstr cs)];
   18.24  
   18.25  
   18.26  fun char_ast_tr [Ast.Variable xstr] =
   18.27 -      (case Syntax.explode_xstr xstr of
   18.28 +      (case Lexicon.explode_xstr xstr of
   18.29          [c] => mk_char c
   18.30        | _ => error ("Single character expected: " ^ xstr))
   18.31    | char_ast_tr asts = raise Ast.AST ("char_ast_tr", asts);
   18.32 @@ -65,7 +66,7 @@
   18.33        Ast.Appl [Ast.Constant @{const_syntax Cons}, mk_char c, mk_string cs];
   18.34  
   18.35  fun string_ast_tr [Ast.Variable xstr] =
   18.36 -      (case Syntax.explode_xstr xstr of
   18.37 +      (case Lexicon.explode_xstr xstr of
   18.38          [] =>
   18.39            Ast.Appl
   18.40              [Ast.Constant @{syntax_const "_constrain"},
    19.1 --- a/src/HOL/Tools/typedef.ML	Fri Apr 08 15:48:14 2011 +0200
    19.2 +++ b/src/HOL/Tools/typedef.ML	Fri Apr 08 16:34:14 2011 +0200
    19.3 @@ -144,7 +144,7 @@
    19.4        error ("Not a set type: " ^ quote (Syntax.string_of_typ lthy setT));
    19.5  
    19.6      val goal = mk_inhabited set;
    19.7 -    val goal_pat = mk_inhabited (Var (the_default (bname, 0) (Syntax.read_variable bname), setT));
    19.8 +    val goal_pat = mk_inhabited (Var (the_default (bname, 0) (Lexicon.read_variable bname), setT));
    19.9  
   19.10  
   19.11      (* lhs *)
    20.1 --- a/src/HOL/ex/Binary.thy	Fri Apr 08 15:48:14 2011 +0200
    20.2 +++ b/src/HOL/ex/Binary.thy	Fri Apr 08 16:34:14 2011 +0200
    20.3 @@ -191,11 +191,11 @@
    20.4  parse_translation {*
    20.5  let
    20.6    val syntax_consts =
    20.7 -    map_aterms (fn Const (c, T) => Const (Syntax.mark_const c, T) | a => a);
    20.8 +    map_aterms (fn Const (c, T) => Const (Lexicon.mark_const c, T) | a => a);
    20.9  
   20.10    fun binary_tr [Const (num, _)] =
   20.11          let
   20.12 -          val {leading_zeros = z, value = n, ...} = Syntax.read_xnum num;
   20.13 +          val {leading_zeros = z, value = n, ...} = Lexicon.read_xnum num;
   20.14            val _ = z = 0 andalso n >= 0 orelse error ("Bad binary number: " ^ num);
   20.15          in syntax_consts (mk_binary n) end
   20.16      | binary_tr ts = raise TERM ("binary_tr", ts);
    21.1 --- a/src/HOL/ex/Numeral.thy	Fri Apr 08 15:48:14 2011 +0200
    21.2 +++ b/src/HOL/ex/Numeral.thy	Fri Apr 08 16:34:14 2011 +0200
    21.3 @@ -285,7 +285,7 @@
    21.4      else raise Match;
    21.5    fun numeral_tr [Free (num, _)] =
    21.6          let
    21.7 -          val {leading_zeros, value, ...} = Syntax.read_xnum num;
    21.8 +          val {leading_zeros, value, ...} = Lexicon.read_xnum num;
    21.9            val _ = leading_zeros = 0 andalso value > 0
   21.10              orelse error ("Bad numeral: " ^ num);
   21.11          in Const (@{const_name of_num}, @{typ num} --> dummyT) $ num_of_int value end
    22.1 --- a/src/Pure/Isar/expression.ML	Fri Apr 08 15:48:14 2011 +0200
    22.2 +++ b/src/Pure/Isar/expression.ML	Fri Apr 08 16:34:14 2011 +0200
    22.3 @@ -613,7 +613,7 @@
    22.4  
    22.5  (* achieve plain syntax for locale predicates (without "PROP") *)
    22.6  
    22.7 -fun aprop_tr' n c = (Syntax.mark_const c, fn ctxt => fn args =>
    22.8 +fun aprop_tr' n c = (Lexicon.mark_const c, fn ctxt => fn args =>
    22.9    if length args = n then
   22.10      Syntax.const "_aprop" $   (* FIXME avoid old-style early externing (!??) *)
   22.11        Term.list_comb (Syntax.free (Consts.extern (ProofContext.consts_of ctxt) c), args)
    23.1 --- a/src/Pure/Isar/proof_context.ML	Fri Apr 08 15:48:14 2011 +0200
    23.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Apr 08 16:34:14 2011 +0200
    23.3 @@ -447,7 +447,7 @@
    23.4      val tsig = tsig_of ctxt;
    23.5      val (c, pos) = token_content text;
    23.6    in
    23.7 -    if Syntax.is_tid c then
    23.8 +    if Lexicon.is_tid c then
    23.9       (Context_Position.report ctxt pos Markup.tfree;
   23.10        TFree (c, default_sort ctxt (c, ~1)))
   23.11      else
   23.12 @@ -924,7 +924,7 @@
   23.13    fold_map (fn (b, raw_T, mx) => fn ctxt =>
   23.14      let
   23.15        val x = Name.of_binding b;
   23.16 -      val _ = Syntax.is_identifier (no_skolem internal x) orelse
   23.17 +      val _ = Lexicon.is_identifier (no_skolem internal x) orelse
   23.18          error ("Illegal variable name: " ^ quote (Binding.str_of b));
   23.19  
   23.20        fun cond_tvars T =
   23.21 @@ -949,7 +949,7 @@
   23.22  fun const_ast_tr intern ctxt [Ast.Variable c] =
   23.23        let
   23.24          val Const (c', _) = read_const_proper ctxt false c;
   23.25 -        val d = if intern then Syntax.mark_const c' else c;
   23.26 +        val d = if intern then Lexicon.mark_const c' else c;
   23.27        in Ast.Constant d end
   23.28    | const_ast_tr _ _ asts = raise Ast.AST ("const_ast_tr", asts);
   23.29  
   23.30 @@ -978,13 +978,13 @@
   23.31  local
   23.32  
   23.33  fun type_syntax (Type (c, args), mx) =
   23.34 -      SOME (Local_Syntax.Type, (Syntax.mark_type c, Mixfix.make_type (length args), mx))
   23.35 +      SOME (Local_Syntax.Type, (Lexicon.mark_type c, Mixfix.make_type (length args), mx))
   23.36    | type_syntax _ = NONE;
   23.37  
   23.38  fun const_syntax _ (Free (x, T), mx) = SOME (Local_Syntax.Fixed, (x, T, mx))
   23.39    | const_syntax ctxt (Const (c, _), mx) =
   23.40        (case try (Consts.type_scheme (consts_of ctxt)) c of
   23.41 -        SOME T => SOME (Local_Syntax.Const, (Syntax.mark_const c, T, mx))
   23.42 +        SOME T => SOME (Local_Syntax.Const, (Lexicon.mark_const c, T, mx))
   23.43        | NONE => NONE)
   23.44    | const_syntax _ _ = NONE;
   23.45  
    24.1 --- a/src/Pure/Isar/token.ML	Fri Apr 08 15:48:14 2011 +0200
    24.2 +++ b/src/Pure/Isar/token.ML	Fri Apr 08 16:34:14 2011 +0200
    24.3 @@ -279,7 +279,7 @@
    24.4  fun ident_or_symbolic "begin" = false
    24.5    | ident_or_symbolic ":" = true
    24.6    | ident_or_symbolic "::" = true
    24.7 -  | ident_or_symbolic s = Syntax.is_identifier s orelse is_symid s;
    24.8 +  | ident_or_symbolic s = Lexicon.is_identifier s orelse is_symid s;
    24.9  
   24.10  
   24.11  (* scan verbatim text *)
   24.12 @@ -335,13 +335,13 @@
   24.13        (Scan.max token_leq
   24.14          (Scan.literal lex2 >> pair Command)
   24.15          (Scan.literal lex1 >> pair Keyword))
   24.16 -      (Syntax.scan_longid >> pair LongIdent ||
   24.17 -        Syntax.scan_id >> pair Ident ||
   24.18 -        Syntax.scan_var >> pair Var ||
   24.19 -        Syntax.scan_tid >> pair TypeIdent ||
   24.20 -        Syntax.scan_tvar >> pair TypeVar ||
   24.21 -        Syntax.scan_float >> pair Float ||
   24.22 -        Syntax.scan_nat >> pair Nat ||
   24.23 +      (Lexicon.scan_longid >> pair LongIdent ||
   24.24 +        Lexicon.scan_id >> pair Ident ||
   24.25 +        Lexicon.scan_var >> pair Var ||
   24.26 +        Lexicon.scan_tid >> pair TypeIdent ||
   24.27 +        Lexicon.scan_tvar >> pair TypeVar ||
   24.28 +        Lexicon.scan_float >> pair Float ||
   24.29 +        Lexicon.scan_nat >> pair Nat ||
   24.30          scan_symid >> pair SymIdent) >> uncurry token));
   24.31  
   24.32  fun recover msg =
    25.1 --- a/src/Pure/ML/ml_antiquote.ML	Fri Apr 08 15:48:14 2011 +0200
    25.2 +++ b/src/Pure/ML/ml_antiquote.ML	Fri Apr 08 16:34:14 2011 +0200
    25.3 @@ -105,7 +105,7 @@
    25.4  
    25.5  fun class syn = Args.context -- Scan.lift Args.name_source >> (fn (ctxt, s) =>
    25.6    ProofContext.read_class ctxt s
    25.7 -  |> syn ? Syntax.mark_class
    25.8 +  |> syn ? Lexicon.mark_class
    25.9    |> ML_Syntax.print_string);
   25.10  
   25.11  val _ = inline "class" (class false);
   25.12 @@ -131,7 +131,7 @@
   25.13  val _ = inline "type_name" (type_name "logical type" (fn (c, Type.LogicalType _) => c));
   25.14  val _ = inline "type_abbrev" (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c));
   25.15  val _ = inline "nonterminal" (type_name "nonterminal" (fn (c, Type.Nonterminal) => c));
   25.16 -val _ = inline "type_syntax" (type_name "type" (fn (c, _) => Syntax.mark_type c));
   25.17 +val _ = inline "type_syntax" (type_name "type" (fn (c, _) => Lexicon.mark_type c));
   25.18  
   25.19  
   25.20  (* constants *)
   25.21 @@ -146,7 +146,7 @@
   25.22  
   25.23  val _ = inline "const_name" (const_name (fn (consts, c) => (Consts.the_type consts c; c)));
   25.24  val _ = inline "const_abbrev" (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c)));
   25.25 -val _ = inline "const_syntax" (const_name (fn (_, c) => Syntax.mark_const c));
   25.26 +val _ = inline "const_syntax" (const_name (fn (_, c) => Lexicon.mark_const c));
   25.27  
   25.28  
   25.29  val _ = inline "syntax_const"
    26.1 --- a/src/Pure/ML/ml_syntax.ML	Fri Apr 08 15:48:14 2011 +0200
    26.2 +++ b/src/Pure/ML/ml_syntax.ML	Fri Apr 08 16:34:14 2011 +0200
    26.3 @@ -34,7 +34,7 @@
    26.4  
    26.5  (* reserved words *)
    26.6  
    26.7 -val reserved_names = filter Syntax.is_ascii_identifier ML_Lex.keywords;
    26.8 +val reserved_names = filter Lexicon.is_ascii_identifier ML_Lex.keywords;
    26.9  val reserved = Name.make_context reserved_names;
   26.10  val is_reserved = Name.is_declared reserved;
   26.11  
   26.12 @@ -42,7 +42,7 @@
   26.13  (* identifiers *)
   26.14  
   26.15  fun is_identifier name =
   26.16 -  not (is_reserved name) andalso Syntax.is_ascii_identifier name;
   26.17 +  not (is_reserved name) andalso Lexicon.is_ascii_identifier name;
   26.18  
   26.19  
   26.20  (* literal output -- unformatted *)
    27.1 --- a/src/Pure/Proof/proof_syntax.ML	Fri Apr 08 15:48:14 2011 +0200
    27.2 +++ b/src/Pure/Proof/proof_syntax.ML	Fri Apr 08 16:34:14 2011 +0200
    27.3 @@ -66,8 +66,8 @@
    27.4         ("", paramT --> paramsT, Delimfix "_")]
    27.5    |> Sign.add_modesyntax_i (Symbol.xsymbolsN, true)
    27.6        [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<Lambda>_./ _)", [0, 3], 3)),
    27.7 -       (Syntax.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\<cdot>/ _)", [4, 5], 4)),
    27.8 -       (Syntax.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\<bullet>/ _)", [4, 5], 4))]
    27.9 +       (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\<cdot>/ _)", [4, 5], 4)),
   27.10 +       (Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\<bullet>/ _)", [4, 5], 4))]
   27.11    |> Sign.add_modesyntax_i ("latex", false)
   27.12        [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<^bold>\\<lambda>_./ _)", [0, 3], 3))]
   27.13    |> Sign.add_trrules (map Syntax.Parse_Print_Rule
   27.14 @@ -80,10 +80,10 @@
   27.15         (Ast.mk_appl (Ast.Constant "_Lam")
   27.16            [Ast.mk_appl (Ast.Constant "_Lam1")
   27.17              [Ast.Variable "x", Ast.Variable "A"], Ast.Variable "B"],
   27.18 -        Ast.mk_appl (Ast.Constant (Syntax.mark_const "AbsP")) [Ast.Variable "A",
   27.19 +        Ast.mk_appl (Ast.Constant (Lexicon.mark_const "AbsP")) [Ast.Variable "A",
   27.20            (Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "B"])]),
   27.21         (Ast.mk_appl (Ast.Constant "_Lam") [Ast.Variable "x", Ast.Variable "A"],
   27.22 -        Ast.mk_appl (Ast.Constant (Syntax.mark_const "Abst"))
   27.23 +        Ast.mk_appl (Ast.Constant (Lexicon.mark_const "Abst"))
   27.24            [(Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "A"])])]);
   27.25  
   27.26  
    28.1 --- a/src/Pure/Syntax/lexicon.ML	Fri Apr 08 15:48:14 2011 +0200
    28.2 +++ b/src/Pure/Syntax/lexicon.ML	Fri Apr 08 16:34:14 2011 +0200
    28.3 @@ -4,10 +4,11 @@
    28.4  Lexer for the inner Isabelle syntax (terms and types).
    28.5  *)
    28.6  
    28.7 -signature LEXICON0 =
    28.8 +signature LEXICON =
    28.9  sig
   28.10    val is_identifier: string -> bool
   28.11    val is_ascii_identifier: string -> bool
   28.12 +  val is_xid: string -> bool
   28.13    val is_tid: string -> bool
   28.14    val scan_id: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
   28.15    val scan_longid: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
   28.16 @@ -19,37 +20,6 @@
   28.17    val scan_bin: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
   28.18    val scan_var: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
   28.19    val scan_tvar: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
   28.20 -  val implode_xstr: string list -> string
   28.21 -  val explode_xstr: string -> string list
   28.22 -  val read_indexname: string -> indexname
   28.23 -  val read_var: string -> term
   28.24 -  val read_variable: string -> indexname option
   28.25 -  val const: string -> term
   28.26 -  val free: string -> term
   28.27 -  val var: indexname -> term
   28.28 -  val read_nat: string -> int option
   28.29 -  val read_int: string -> int option
   28.30 -  val read_xnum: string -> {radix: int, leading_zeros: int, value: int}
   28.31 -  val read_float: string -> {mant: int, exp: int}
   28.32 -  val mark_class: string -> string val unmark_class: string -> string
   28.33 -  val mark_type: string -> string val unmark_type: string -> string
   28.34 -  val mark_const: string -> string val unmark_const: string -> string
   28.35 -  val mark_fixed: string -> string val unmark_fixed: string -> string
   28.36 -  val unmark:
   28.37 -   {case_class: string -> 'a,
   28.38 -    case_type: string -> 'a,
   28.39 -    case_const: string -> 'a,
   28.40 -    case_fixed: string -> 'a,
   28.41 -    case_default: string -> 'a} -> string -> 'a
   28.42 -  val is_marked: string -> bool
   28.43 -  val dummy_type: term
   28.44 -  val fun_type: term
   28.45 -end;
   28.46 -
   28.47 -signature LEXICON =
   28.48 -sig
   28.49 -  include LEXICON0
   28.50 -  val is_xid: string -> bool
   28.51    datatype token_kind =
   28.52      Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy |
   28.53      NumSy | FloatSy | XNumSy | StrSy | Space | Comment | EOF
   28.54 @@ -73,7 +43,32 @@
   28.55    val matching_tokens: token * token -> bool
   28.56    val valued_token: token -> bool
   28.57    val predef_term: string -> token option
   28.58 +  val implode_xstr: string list -> string
   28.59 +  val explode_xstr: string -> string list
   28.60    val tokenize: Scan.lexicon -> bool -> Symbol_Pos.T list -> token list
   28.61 +  val read_indexname: string -> indexname
   28.62 +  val const: string -> term
   28.63 +  val free: string -> term
   28.64 +  val var: indexname -> term
   28.65 +  val read_var: string -> term
   28.66 +  val read_variable: string -> indexname option
   28.67 +  val read_nat: string -> int option
   28.68 +  val read_int: string -> int option
   28.69 +  val read_xnum: string -> {radix: int, leading_zeros: int, value: int}
   28.70 +  val read_float: string -> {mant: int, exp: int}
   28.71 +  val mark_class: string -> string val unmark_class: string -> string
   28.72 +  val mark_type: string -> string val unmark_type: string -> string
   28.73 +  val mark_const: string -> string val unmark_const: string -> string
   28.74 +  val mark_fixed: string -> string val unmark_fixed: string -> string
   28.75 +  val unmark:
   28.76 +   {case_class: string -> 'a,
   28.77 +    case_type: string -> 'a,
   28.78 +    case_const: string -> 'a,
   28.79 +    case_fixed: string -> 'a,
   28.80 +    case_default: string -> 'a} -> string -> 'a
   28.81 +  val is_marked: string -> bool
   28.82 +  val dummy_type: term
   28.83 +  val fun_type: term
   28.84  end;
   28.85  
   28.86  structure Lexicon: LEXICON =
   28.87 @@ -352,37 +347,6 @@
   28.88    in Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode (str, Position.none)) end;
   28.89  
   28.90  
   28.91 -(* logical entities *)
   28.92 -
   28.93 -fun marker s = (prefix s, unprefix s);
   28.94 -
   28.95 -val (mark_class, unmark_class) = marker "\\<^class>";
   28.96 -val (mark_type, unmark_type) = marker "\\<^type>";
   28.97 -val (mark_const, unmark_const) = marker "\\<^const>";
   28.98 -val (mark_fixed, unmark_fixed) = marker "\\<^fixed>";
   28.99 -
  28.100 -fun unmark {case_class, case_type, case_const, case_fixed, case_default} s =
  28.101 -  (case try unmark_class s of
  28.102 -    SOME c => case_class c
  28.103 -  | NONE =>
  28.104 -      (case try unmark_type s of
  28.105 -        SOME c => case_type c
  28.106 -      | NONE =>
  28.107 -          (case try unmark_const s of
  28.108 -            SOME c => case_const c
  28.109 -          | NONE =>
  28.110 -              (case try unmark_fixed s of
  28.111 -                SOME c => case_fixed c
  28.112 -              | NONE => case_default s))));
  28.113 -
  28.114 -val is_marked =
  28.115 -  unmark {case_class = K true, case_type = K true, case_const = K true,
  28.116 -    case_fixed = K true, case_default = K false};
  28.117 -
  28.118 -val dummy_type = const (mark_type "dummy");
  28.119 -val fun_type = const (mark_type "fun");
  28.120 -
  28.121 -
  28.122  (* read numbers *)
  28.123  
  28.124  local
  28.125 @@ -456,4 +420,35 @@
  28.126      exp = length fracpart}
  28.127    end;
  28.128  
  28.129 +
  28.130 +(* marked logical entities *)
  28.131 +
  28.132 +fun marker s = (prefix s, unprefix s);
  28.133 +
  28.134 +val (mark_class, unmark_class) = marker "\\<^class>";
  28.135 +val (mark_type, unmark_type) = marker "\\<^type>";
  28.136 +val (mark_const, unmark_const) = marker "\\<^const>";
  28.137 +val (mark_fixed, unmark_fixed) = marker "\\<^fixed>";
  28.138 +
  28.139 +fun unmark {case_class, case_type, case_const, case_fixed, case_default} s =
  28.140 +  (case try unmark_class s of
  28.141 +    SOME c => case_class c
  28.142 +  | NONE =>
  28.143 +      (case try unmark_type s of
  28.144 +        SOME c => case_type c
  28.145 +      | NONE =>
  28.146 +          (case try unmark_const s of
  28.147 +            SOME c => case_const c
  28.148 +          | NONE =>
  28.149 +              (case try unmark_fixed s of
  28.150 +                SOME c => case_fixed c
  28.151 +              | NONE => case_default s))));
  28.152 +
  28.153 +val is_marked =
  28.154 +  unmark {case_class = K true, case_type = K true, case_const = K true,
  28.155 +    case_fixed = K true, case_default = K false};
  28.156 +
  28.157 +val dummy_type = const (mark_type "dummy");
  28.158 +val fun_type = const (mark_type "fun");
  28.159 +
  28.160  end;
    29.1 --- a/src/Pure/Syntax/local_syntax.ML	Fri Apr 08 15:48:14 2011 +0200
    29.2 +++ b/src/Pure/Syntax/local_syntax.ML	Fri Apr 08 16:34:14 2011 +0200
    29.3 @@ -83,7 +83,7 @@
    29.4    | prep_mixfix add mode (Type, decl as (x, _, _)) = SOME ((x, false), ((true, add, mode), decl))
    29.5    | prep_mixfix add mode (Const, decl as (x, _, _)) = SOME ((x, false), ((false, add, mode), decl))
    29.6    | prep_mixfix add mode (Fixed, (x, T, mx)) =
    29.7 -      SOME ((x, true), ((false, add, mode), (Syntax.mark_fixed x, T, mx)));
    29.8 +      SOME ((x, true), ((false, add, mode), (Lexicon.mark_fixed x, T, mx)));
    29.9  
   29.10  fun prep_struct (Fixed, (c, _, Structure)) = SOME c
   29.11    | prep_struct (_, (c, _, Structure)) = error ("Bad mixfix declaration for " ^ quote c)
    30.1 --- a/src/Pure/Syntax/syntax.ML	Fri Apr 08 15:48:14 2011 +0200
    30.2 +++ b/src/Pure/Syntax/syntax.ML	Fri Apr 08 16:34:14 2011 +0200
    30.3 @@ -7,8 +7,10 @@
    30.4  
    30.5  signature SYNTAX =
    30.6  sig
    30.7 -  include LEXICON0
    30.8    val max_pri: int
    30.9 +  val const: string -> term
   30.10 +  val free: string -> term
   30.11 +  val var: indexname -> term
   30.12    val root: string Config.T
   30.13    val positions_raw: Config.raw
   30.14    val positions: bool Config.T
   30.15 @@ -143,6 +145,11 @@
   30.16  
   30.17  val max_pri = Syntax_Ext.max_pri;
   30.18  
   30.19 +val const = Lexicon.const;
   30.20 +val free = Lexicon.free;
   30.21 +val var = Lexicon.var;
   30.22 +
   30.23 +
   30.24  
   30.25  (** inner syntax operations **)
   30.26  
   30.27 @@ -719,11 +726,5 @@
   30.28  val update_trrules = ext_syntax Syntax_Ext.syn_ext_rules o check_rules;
   30.29  val remove_trrules = remove_syntax mode_default o Syntax_Ext.syn_ext_rules o check_rules;
   30.30  
   30.31 -
   30.32 -(*export parts of internal Syntax structures*)
   30.33 -val syntax_tokenize = tokenize;
   30.34 -open Lexicon;
   30.35 -val tokenize = syntax_tokenize;
   30.36 -
   30.37  end;
   30.38  
    31.1 --- a/src/Pure/Syntax/syntax_phases.ML	Fri Apr 08 15:48:14 2011 +0200
    31.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Fri Apr 08 16:34:14 2011 +0200
    31.3 @@ -434,9 +434,9 @@
    31.4      fun term_of (Type (a, Ts)) =
    31.5            Term.list_comb (Lexicon.const (Lexicon.mark_type a), map term_of Ts)
    31.6        | term_of (TFree (x, S)) =
    31.7 -          if is_some (Term_Position.decode x) then Lexicon.free x
    31.8 -          else of_sort (Lexicon.const "_tfree" $ Lexicon.free x) S
    31.9 -      | term_of (TVar (xi, S)) = of_sort (Lexicon.const "_tvar" $ Lexicon.var xi) S;
   31.10 +          if is_some (Term_Position.decode x) then Syntax.free x
   31.11 +          else of_sort (Lexicon.const "_tfree" $ Syntax.free x) S
   31.12 +      | term_of (TVar (xi, S)) = of_sort (Lexicon.const "_tvar" $ Syntax.var xi) S;
   31.13    in term_of ty end;
   31.14  
   31.15  
   31.16 @@ -514,11 +514,11 @@
   31.17      fun prune_typs (t_seen as (Const _, _)) = t_seen
   31.18        | prune_typs (t as Free (x, ty), seen) =
   31.19            if ty = dummyT then (t, seen)
   31.20 -          else if not show_free_types orelse member (op aconv) seen t then (Lexicon.free x, seen)
   31.21 +          else if not show_free_types orelse member (op aconv) seen t then (Syntax.free x, seen)
   31.22            else (t, t :: seen)
   31.23        | prune_typs (t as Var (xi, ty), seen) =
   31.24            if ty = dummyT then (t, seen)
   31.25 -          else if not show_free_types orelse member (op aconv) seen t then (Lexicon.var xi, seen)
   31.26 +          else if not show_free_types orelse member (op aconv) seen t then (Syntax.var xi, seen)
   31.27            else (t, t :: seen)
   31.28        | prune_typs (t_seen as (Bound _, _)) = t_seen
   31.29        | prune_typs (Abs (x, ty, t), seen) =
   31.30 @@ -534,11 +534,11 @@
   31.31        (case strip_comb tm of
   31.32          (t as Abs _, ts) => Ast.mk_appl (ast_of (Syntax_Trans.abs_tr' ctxt t)) (map ast_of ts)
   31.33        | ((c as Const ("_free", _)), Free (x, T) :: ts) =>
   31.34 -          Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
   31.35 +          Ast.mk_appl (constrain (c $ Syntax.free x) T) (map ast_of ts)
   31.36        | ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
   31.37 -          Ast.mk_appl (constrain (c $ Lexicon.var xi) T) (map ast_of ts)
   31.38 +          Ast.mk_appl (constrain (c $ Syntax.var xi) T) (map ast_of ts)
   31.39        | ((c as Const ("_bound", _)), Free (x, T) :: ts) =>
   31.40 -          Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
   31.41 +          Ast.mk_appl (constrain (c $ Syntax.free x) T) (map ast_of ts)
   31.42        | (Const ("_idtdummy", T), ts) =>
   31.43            Ast.mk_appl (constrain (Lexicon.const "_idtdummy") T) (map ast_of ts)
   31.44        | (const as Const (c, T), ts) =>
    32.1 --- a/src/Pure/Thy/latex.ML	Fri Apr 08 15:48:14 2011 +0200
    32.2 +++ b/src/Pure/Thy/latex.ML	Fri Apr 08 16:34:14 2011 +0200
    32.3 @@ -130,7 +130,7 @@
    32.4      if invisible_token tok then ""
    32.5      else if Token.is_kind Token.Command tok then
    32.6        "\\isacommand{" ^ output_syms s ^ "}"
    32.7 -    else if Token.is_kind Token.Keyword tok andalso Syntax.is_ascii_identifier s then
    32.8 +    else if Token.is_kind Token.Keyword tok andalso Lexicon.is_ascii_identifier s then
    32.9        "\\isakeyword{" ^ output_syms s ^ "}"
   32.10      else if Token.is_kind Token.String tok then
   32.11        output_syms s |> enclose
    33.1 --- a/src/Pure/Thy/thy_syntax.ML	Fri Apr 08 15:48:14 2011 +0200
    33.2 +++ b/src/Pure/Thy/thy_syntax.ML	Fri Apr 08 16:34:14 2011 +0200
    33.3 @@ -65,7 +65,7 @@
    33.4    | Token.EOF           => Markup.control;
    33.5  
    33.6  fun token_markup tok =
    33.7 -  if Token.keyword_with (not o Syntax.is_identifier) tok then Markup.operator
    33.8 +  if Token.keyword_with (not o Lexicon.is_identifier) tok then Markup.operator
    33.9    else
   33.10      let
   33.11        val kind = Token.kind_of tok;
    34.1 --- a/src/Pure/consts.ML	Fri Apr 08 15:48:14 2011 +0200
    34.2 +++ b/src/Pure/consts.ML	Fri Apr 08 16:34:14 2011 +0200
    34.3 @@ -132,12 +132,12 @@
    34.4  val extern = Name_Space.extern o space_of;
    34.5  
    34.6  fun intern_syntax consts s =
    34.7 -  (case try Syntax.unmark_const s of
    34.8 +  (case try Lexicon.unmark_const s of
    34.9      SOME c => c
   34.10    | NONE => intern consts s);
   34.11  
   34.12  fun extern_syntax consts s =
   34.13 -  (case try Syntax.unmark_const s of
   34.14 +  (case try Lexicon.unmark_const s of
   34.15      SOME c => extern consts c
   34.16    | NONE => s);
   34.17  
    35.1 --- a/src/Pure/pure_thy.ML	Fri Apr 08 15:48:14 2011 +0200
    35.2 +++ b/src/Pure/pure_thy.ML	Fri Apr 08 16:34:14 2011 +0200
    35.3 @@ -16,8 +16,8 @@
    35.4  val typ = Simple_Syntax.read_typ;
    35.5  val prop = Simple_Syntax.read_prop;
    35.6  
    35.7 -val tycon = Syntax.mark_type;
    35.8 -val const = Syntax.mark_const;
    35.9 +val tycon = Lexicon.mark_type;
   35.10 +val const = Lexicon.mark_const;
   35.11  
   35.12  val typeT = Syntax_Ext.typeT;
   35.13  val spropT = Syntax_Ext.spropT;
    36.1 --- a/src/Pure/sign.ML	Fri Apr 08 15:48:14 2011 +0200
    36.2 +++ b/src/Pure/sign.ML	Fri Apr 08 16:34:14 2011 +0200
    36.3 @@ -334,7 +334,7 @@
    36.4  fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
    36.5    let
    36.6      fun type_syntax (b, n, mx) =
    36.7 -      (Syntax.mark_type (Name_Space.full_name naming b), Mixfix.make_type n, mx);
    36.8 +      (Lexicon.mark_type (Name_Space.full_name naming b), Mixfix.make_type n, mx);
    36.9      val syn' = Syntax.update_type_gram true Syntax.mode_default (map type_syntax types) syn;
   36.10      val tsig' = fold (fn (a, n, _) => Type.add_type naming (a, n)) types tsig;
   36.11    in (naming, syn', tsig', consts) end);
   36.12 @@ -373,7 +373,7 @@
   36.13  fun type_notation add mode args =
   36.14    let
   36.15      fun type_syntax (Type (c, args), mx) =
   36.16 -          SOME (Syntax.mark_type c, Mixfix.make_type (length args), mx)
   36.17 +          SOME (Lexicon.mark_type c, Mixfix.make_type (length args), mx)
   36.18        | type_syntax _ = NONE;
   36.19    in map_syn (Syntax.update_type_gram add mode (map_filter type_syntax args)) end;
   36.20  
   36.21 @@ -381,7 +381,7 @@
   36.22    let
   36.23      fun const_syntax (Const (c, _), mx) =
   36.24            (case try (Consts.type_scheme (consts_of thy)) c of
   36.25 -            SOME T => SOME (Syntax.mark_const c, T, mx)
   36.26 +            SOME T => SOME (Lexicon.mark_const c, T, mx)
   36.27            | NONE => NONE)
   36.28        | const_syntax _ = NONE;
   36.29    in gen_syntax (Syntax.update_const_gram add) (K I) mode (map_filter const_syntax args) thy end;
   36.30 @@ -401,7 +401,7 @@
   36.31          val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
   36.32            cat_error msg ("in declaration of constant " ^ quote (Binding.str_of b));
   36.33          val T' = Logic.varifyT_global T;
   36.34 -      in ((b, T'), (Syntax.mark_const c, T', mx), Const (c, T)) end;
   36.35 +      in ((b, T'), (Lexicon.mark_const c, T', mx), Const (c, T)) end;
   36.36      val args = map prep raw_args;
   36.37    in
   36.38      thy
    37.1 --- a/src/Pure/tactic.ML	Fri Apr 08 15:48:14 2011 +0200
    37.2 +++ b/src/Pure/tactic.ML	Fri Apr 08 16:34:14 2011 +0200
    37.3 @@ -318,7 +318,7 @@
    37.4  
    37.5  (*Renaming of parameters in a subgoal*)
    37.6  fun rename_tac xs i =
    37.7 -  case Library.find_first (not o Syntax.is_identifier) xs of
    37.8 +  case Library.find_first (not o Lexicon.is_identifier) xs of
    37.9        SOME x => error ("Not an identifier: " ^ x)
   37.10      | NONE => PRIMITIVE (Thm.rename_params_rule (xs, i));
   37.11  
    38.1 --- a/src/ZF/Tools/datatype_package.ML	Fri Apr 08 15:48:14 2011 +0200
    38.2 +++ b/src/ZF/Tools/datatype_package.ML	Fri Apr 08 16:34:14 2011 +0200
    38.3 @@ -130,7 +130,7 @@
    38.4  
    38.5    (*The function variable for a single constructor*)
    38.6    fun add_case ((_, T, _), name, args, _) (opno, cases) =
    38.7 -    if Syntax.is_identifier name then
    38.8 +    if Lexicon.is_identifier name then
    38.9        (opno, (Free (case_varname ^ "_" ^ name, T), args) :: cases)
   38.10      else
   38.11        (opno + 1, (Free (case_varname ^ "_op_" ^ string_of_int opno, T), args)
    39.1 --- a/src/ZF/Tools/inductive_package.ML	Fri Apr 08 15:48:14 2011 +0200
    39.2 +++ b/src/ZF/Tools/inductive_package.ML	Fri Apr 08 16:34:14 2011 +0200
    39.3 @@ -78,7 +78,7 @@
    39.4    and (Const(_,recT),rec_params) = strip_comb (hd rec_tms);
    39.5  
    39.6    val rec_base_names = map Long_Name.base_name rec_names;
    39.7 -  val dummy = assert_all Syntax.is_identifier rec_base_names
    39.8 +  val dummy = assert_all Lexicon.is_identifier rec_base_names
    39.9      (fn a => "Base name of recursive set not an identifier: " ^ a);
   39.10  
   39.11    local (*Checking the introduction rules*)
    40.1 --- a/src/ZF/Tools/numeral_syntax.ML	Fri Apr 08 15:48:14 2011 +0200
    40.2 +++ b/src/ZF/Tools/numeral_syntax.ML	Fri Apr 08 16:34:14 2011 +0200
    40.3 @@ -71,7 +71,7 @@
    40.4  (* translation of integer constant tokens to and from binary *)
    40.5  
    40.6  fun int_tr [t as Free (str, _)] =
    40.7 -      Syntax.const @{const_syntax integ_of} $ mk_bin (#value (Syntax.read_xnum str))
    40.8 +      Syntax.const @{const_syntax integ_of} $ mk_bin (#value (Lexicon.read_xnum str))
    40.9    | int_tr ts = raise TERM ("int_tr", ts);
   40.10  
   40.11  fun int_tr' [t] = Syntax.const @{syntax_const "_Int"} $ Syntax.free (show_int t)