# HG changeset patch
# User wenzelm
# Date 1187021422 -7200
# Node ID d7ee11ba1534d0ff151b65bd445cd8e3baf588e0
# Parent  08db58fd637413e4a6efb42efb84f506592e8091
Lexicon.read_indexname/nat/variable;

diff -r 08db58fd6374 -r d7ee11ba1534 src/Pure/Isar/args.ML
--- 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 *)
diff -r 08db58fd6374 -r d7ee11ba1534 src/Pure/Isar/rule_cases.ML
--- 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);
diff -r 08db58fd6374 -r d7ee11ba1534 src/Pure/ProofGeneral/proof_general_emacs.ML
--- 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
diff -r 08db58fd6374 -r d7ee11ba1534 src/Pure/ProofGeneral/proof_general_pgip.ML
--- 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
diff -r 08db58fd6374 -r d7ee11ba1534 src/Pure/Thy/html.ML
--- 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
diff -r 08db58fd6374 -r d7ee11ba1534 src/Pure/tactic.ML
--- 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