1.1 --- a/src/Pure/Isar/args.ML	Mon Aug 13 18:10:20 2007 +0200
     1.2 +++ b/src/Pure/Isar/args.ML	Mon Aug 13 18:10:22 2007 +0200
     1.3 @@ -280,9 +280,9 @@
     1.4  val symbol = symbolic >> sym_of;
     1.5  val liberal_name = symbol || name;
     1.6  
     1.7 -val nat = some_ident Syntax.read_nat;
     1.8 +val nat = some_ident Lexicon.read_nat;
     1.9  val int = Scan.optional ($$$ "-" >> K ~1) 1 -- nat >> op *;
    1.10 -val var = some_ident Syntax.read_variable;
    1.11 +val var = some_ident Lexicon.read_variable;
    1.12  
    1.13  
    1.14  (* enumerations *)

     2.1 --- a/src/Pure/Isar/rule_cases.ML	Mon Aug 13 18:10:20 2007 +0200
     2.2 +++ b/src/Pure/Isar/rule_cases.ML	Mon Aug 13 18:10:22 2007 +0200
     2.3 @@ -217,7 +217,7 @@
     2.4    (case AList.lookup (op =) (Thm.get_tags th) (consumes_tagN) of
     2.5      NONE => NONE
     2.6    | SOME s =>
     2.7 -      (case Syntax.read_nat s of SOME n => SOME n
     2.8 +      (case Lexicon.read_nat s of SOME n => SOME n
     2.9        | _ => raise THM ("Malformed 'consumes' tag of theorem", 0, [th])));
    2.10  
    2.11  fun get_consumes th = the_default 0 (lookup_consumes th);

     3.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Aug 13 18:10:20 2007 +0200
     3.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Aug 13 18:10:22 2007 +0200
     3.3 @@ -72,7 +72,7 @@
     3.4    | SOME x' => tagit skolem_tag x');
     3.5  
     3.6  fun var_or_skolem s =
     3.7 -  (case Syntax.read_variable s of
     3.8 +  (case Lexicon.read_variable s of
     3.9      SOME (x, i) =>
    3.10        (case try Name.dest_skolem x of
    3.11          NONE => tagit var_tag s

     4.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Aug 13 18:10:20 2007 +0200
     4.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Aug 13 18:10:22 2007 +0200
     4.3 @@ -86,7 +86,7 @@
     4.4    | SOME x' => tagit skolem_tag x');
     4.5  
     4.6  fun var_or_skolem s =
     4.7 -  (case Syntax.read_variable s of
     4.8 +  (case Lexicon.read_variable s of
     4.9      SOME (x, i) =>
    4.10        (case try Name.dest_skolem x of
    4.11          NONE => tagit var_tag s

     5.1 --- a/src/Pure/Thy/html.ML	Mon Aug 13 18:10:20 2007 +0200
     5.2 +++ b/src/Pure/Thy/html.ML	Mon Aug 13 18:10:22 2007 +0200
     5.3 @@ -250,7 +250,7 @@
     5.4    | SOME x' => style "skolem" x');
     5.5  
     5.6  fun var_or_skolem s =
     5.7 -  (case Syntax.read_variable s of
     5.8 +  (case Lexicon.read_variable s of
     5.9      SOME (x, i) =>
    5.10        (case try Name.dest_skolem x of
    5.11          NONE => style "var" s

     6.1 --- a/src/Pure/tactic.ML	Mon Aug 13 18:10:20 2007 +0200
     6.2 +++ b/src/Pure/tactic.ML	Mon Aug 13 18:10:22 2007 +0200
     6.3 @@ -245,7 +245,7 @@
     6.4  end;
     6.5  
     6.6  fun lift_inst_rule (st, i, sinsts, rule) = lift_inst_rule'
     6.7 -  (st, i, map (apfst Syntax.read_indexname) sinsts, rule);
     6.8 +  (st, i, map (apfst Lexicon.read_indexname) sinsts, rule);
     6.9  
    6.10  (*
    6.11  Like lift_inst_rule but takes terms, not strings, where the terms may contain