Lexicon.read_indexname/nat/variable;

--- a/src/Pure/Isar/args.ML	Mon Aug 13 18:10:20 2007 +0200
+++ b/src/Pure/Isar/args.ML	Mon Aug 13 18:10:22 2007 +0200
@@ -280,9 +280,9 @@
 val symbol = symbolic >> sym_of;
 val liberal_name = symbol || name;
 
-val nat = some_ident Syntax.read_nat;
+val nat = some_ident Lexicon.read_nat;
 val int = Scan.optional ($$$ "-" >> K ~1) 1 -- nat >> op *;
-val var = some_ident Syntax.read_variable;
+val var = some_ident Lexicon.read_variable;
 
 
 (* enumerations *)

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

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

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

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

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