# HG changeset patch
# User wenzelm
# Date 1289674043 -3600
# Node ID 14a2e686bdac1764a92e28a2b8051ceaa7923aae
# Parent  6131d7a78ad3380a706ea75f3ed2dab5a36b3299
eliminated slightly odd pervasive Symbol_Pos.symbol;

diff -r 6131d7a78ad3 -r 14a2e686bdac src/Pure/General/symbol_pos.ML
--- a/src/Pure/General/symbol_pos.ML	Sat Nov 13 19:27:41 2010 +0100
+++ b/src/Pure/General/symbol_pos.ML	Sat Nov 13 19:47:23 2010 +0100
@@ -182,7 +182,6 @@
 
 structure Basic_Symbol_Pos =   (*not open by default*)
 struct
-  val symbol = Symbol_Pos.symbol;
   val $$$ = Symbol_Pos.$$$;
   val ~$$$ = Symbol_Pos.~$$$;
 end;
diff -r 6131d7a78ad3 -r 14a2e686bdac src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Sat Nov 13 19:27:41 2010 +0100
+++ b/src/Pure/Isar/token.ML	Sat Nov 13 19:47:23 2010 +0100
@@ -269,8 +269,8 @@
 val is_sym_char = member (op =) (explode "!#$%&*+-/<=>?@^_|~");
 
 val scan_symid =
-  Scan.many1 (is_sym_char o symbol) ||
-  Scan.one (Symbol.is_symbolic o symbol) >> single;
+  Scan.many1 (is_sym_char o Symbol_Pos.symbol) ||
+  Scan.one (Symbol.is_symbolic o Symbol_Pos.symbol) >> single;
 
 fun is_symid str =
   (case try Symbol.explode str of
@@ -301,8 +301,8 @@
 fun is_space s = Symbol.is_blank s andalso s <> "\n";
 
 val scan_space =
-  Scan.many1 (is_space o symbol) @@@ Scan.optional ($$$ "\n") [] ||
-  Scan.many (is_space o symbol) @@@ $$$ "\n";
+  Scan.many1 (is_space o Symbol_Pos.symbol) @@@ Scan.optional ($$$ "\n") [] ||
+  Scan.many (is_space o Symbol_Pos.symbol) @@@ $$$ "\n";
 
 
 (* scan comment *)
@@ -332,8 +332,8 @@
     scan_verbatim >> token_range Verbatim ||
     scan_comment >> token_range Comment ||
     scan_space >> token Space ||
-    Scan.one (Symbol.is_malformed o symbol) >> (token Malformed o single) ||
-    Scan.one (Symbol.is_sync o symbol) >> (token Sync o single) ||
+    Scan.one (Symbol.is_malformed o Symbol_Pos.symbol) >> (token Malformed o single) ||
+    Scan.one (Symbol.is_sync o Symbol_Pos.symbol) >> (token Sync o single) ||
     (Scan.max token_leq
       (Scan.max token_leq
         (Scan.literal lex2 >> pair Command)
@@ -348,7 +348,7 @@
         scan_symid >> pair SymIdent) >> uncurry token));
 
 fun recover msg =
-  Scan.many ((Symbol.is_regular andf (not o Symbol.is_blank)) o symbol)
+  Scan.many ((Symbol.is_regular andf (not o Symbol.is_blank)) o Symbol_Pos.symbol)
   >> (single o token (Error msg));
 
 in
diff -r 6131d7a78ad3 -r 14a2e686bdac src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Sat Nov 13 19:27:41 2010 +0100
+++ b/src/Pure/ML/ml_lex.ML	Sat Nov 13 19:47:23 2010 +0100
@@ -135,7 +135,7 @@
 
 (* blanks *)
 
-val scan_blank = Scan.one (Symbol.is_ascii_blank o symbol);
+val scan_blank = Scan.one (Symbol.is_ascii_blank o Symbol_Pos.symbol);
 val scan_blanks1 = Scan.repeat1 scan_blank;
 
 
@@ -158,11 +158,15 @@
 local
 
 val scan_letdigs =
-  Scan.many ((Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf Symbol.is_ascii_quasi) o symbol);
+  Scan.many
+    ((Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf Symbol.is_ascii_quasi) o
+      Symbol_Pos.symbol);
 
-val scan_alphanumeric = Scan.one (Symbol.is_ascii_letter o symbol) -- scan_letdigs >> op ::;
+val scan_alphanumeric =
+  Scan.one (Symbol.is_ascii_letter o Symbol_Pos.symbol) -- scan_letdigs >> op ::;
 
-val scan_symbolic = Scan.many1 (member (op =) (explode "!#$%&*+-/:<=>?@\\^`|~") o symbol);
+val scan_symbolic =
+  Scan.many1 (member (op =) (explode "!#$%&*+-/:<=>?@\\^`|~") o Symbol_Pos.symbol);
 
 in
 
@@ -180,8 +184,8 @@
 
 local
 
-val scan_dec = Scan.many1 (Symbol.is_ascii_digit o symbol);
-val scan_hex = Scan.many1 (Symbol.is_ascii_hex o symbol);
+val scan_dec = Scan.many1 (Symbol.is_ascii_digit o Symbol_Pos.symbol);
+val scan_hex = Scan.many1 (Symbol.is_ascii_hex o Symbol_Pos.symbol);
 val scan_sign = Scan.optional ($$$ "~") [];
 val scan_decint = scan_sign @@@ scan_dec;
 
@@ -207,11 +211,11 @@
 local
 
 val scan_escape =
-  Scan.one (member (op =) (explode "\"\\abtnvfr") o symbol) >> single ||
+  Scan.one (member (op =) (explode "\"\\abtnvfr") o Symbol_Pos.symbol) >> single ||
   $$$ "^" @@@ (Scan.one (fn (s, _) => ord "@" <= ord s andalso ord s <= ord "_") >> single) ||
-  Scan.one (Symbol.is_ascii_digit o symbol) --
-    Scan.one (Symbol.is_ascii_digit o symbol) --
-    Scan.one (Symbol.is_ascii_digit o symbol) >> (fn ((a, b), c) => [a, b, c]);
+  Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) --
+    Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) --
+    Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) >> (fn ((a, b), c) => [a, b, c]);
 
 val scan_str =
   Scan.one (fn (s, _) => Symbol.is_regular s andalso s <> "\"" andalso s <> "\\" andalso
@@ -256,7 +260,7 @@
 val scan_antiq = Antiquote.scan || scan_ml >> Antiquote.Text;
 
 fun recover msg =
-  Scan.many (((not o Symbol.is_blank) andf Symbol.is_regular) o symbol)
+  Scan.many (((not o Symbol.is_blank) andf Symbol.is_regular) o Symbol_Pos.symbol)
   >> (fn cs => [token (Error msg) cs]);
 
 in
diff -r 6131d7a78ad3 -r 14a2e686bdac src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Sat Nov 13 19:27:41 2010 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Sat Nov 13 19:47:23 2010 +0100
@@ -103,15 +103,18 @@
 
 fun !!! msg = Symbol_Pos.!!! ("Inner lexical error: " ^ msg);
 
-val scan_id = Scan.one (Symbol.is_letter o symbol) ::: Scan.many (Symbol.is_letdig o symbol);
+val scan_id =
+  Scan.one (Symbol.is_letter o Symbol_Pos.symbol) :::
+  Scan.many (Symbol.is_letdig o Symbol_Pos.symbol);
+
 val scan_longid = scan_id @@@ (Scan.repeat1 ($$$ "." @@@ scan_id) >> flat);
 val scan_tid = $$$ "'" @@@ scan_id;
 
-val scan_nat = Scan.many1 (Symbol.is_digit o symbol);
+val scan_nat = Scan.many1 (Symbol.is_digit o Symbol_Pos.symbol);
 val scan_int = $$$ "-" @@@ scan_nat || scan_nat;
 val scan_natdot = scan_nat @@@ $$$ "." @@@ scan_nat;
 val scan_float = $$$ "-" @@@ scan_natdot || scan_natdot;
-val scan_hex = $$$ "0" @@@ $$$ "x" @@@ Scan.many1 (Symbol.is_ascii_hex o symbol);
+val scan_hex = $$$ "0" @@@ $$$ "x" @@@ Scan.many1 (Symbol.is_ascii_hex o Symbol_Pos.symbol);
 val scan_bin = $$$ "0" @@@ $$$ "b" @@@ Scan.many1 (fn (s, _) => s = "0" orelse s = "1");
 
 val scan_id_nat = scan_id @@@ Scan.optional ($$$ "." @@@ scan_nat) [];
@@ -221,7 +224,9 @@
 
 val scan_chr =
   $$$ "\\" |-- $$$ "'" ||
-  Scan.one ((fn s => s <> "\\" andalso s <> "'" andalso Symbol.is_regular s) o symbol) >> single ||
+  Scan.one
+    ((fn s => s <> "\\" andalso s <> "'" andalso Symbol.is_regular s) o
+      Symbol_Pos.symbol) >> single ||
   $$$ "'" --| Scan.ahead (~$$$ "'");
 
 val scan_str =
@@ -237,7 +242,7 @@
 
 fun explode_xstr str =
   (case Scan.read Symbol_Pos.stopper scan_str_body (Symbol_Pos.explode (str, Position.none)) of
-    SOME cs => map symbol cs
+    SOME cs => map Symbol_Pos.symbol cs
   | _ => error ("Inner lexical error: literal string expected at " ^ quote str));
 
 
@@ -271,7 +276,7 @@
       Symbol_Pos.scan_comment !!! >> token Comment ||
       Scan.max token_leq scan_lit scan_val ||
       scan_str >> token StrSy ||
-      Scan.many1 (Symbol.is_blank o symbol) >> token Space;
+      Scan.many1 (Symbol.is_blank o Symbol_Pos.symbol) >> token Space;
   in
     (case Scan.error
         (Scan.finite Symbol_Pos.stopper (Scan.repeat scan_token)) syms of
@@ -301,8 +306,8 @@
           if Symbol.is_digit c then chop_idx cs (c :: ds)
           else idxname (c :: cs) ds;
 
-    val scan = (scan_id >> map symbol) --
-      Scan.optional ($$$ "." |-- scan_nat >> (nat 0 o map symbol)) ~1;
+    val scan = (scan_id >> map Symbol_Pos.symbol) --
+      Scan.optional ($$$ "." |-- scan_nat >> (nat 0 o map Symbol_Pos.symbol)) ~1;
   in
     scan >>
       (fn (cs, ~1) => chop_idx (rev cs) []
@@ -334,7 +339,7 @@
   let
     val scan =
       $$$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol_Pos.is_eof) >> var ||
-      Scan.many (Symbol.is_regular o symbol) >> (free o implode o map symbol);
+      Scan.many (Symbol.is_regular o Symbol_Pos.symbol) >> (free o implode o map Symbol_Pos.symbol);
   in the (Scan.read Symbol_Pos.stopper scan (Symbol_Pos.explode (str, Position.none))) end;
 
 
@@ -378,7 +383,7 @@
 local
 
 fun nat cs =
-  Option.map (#1 o Library.read_int o map symbol)
+  Option.map (#1 o Library.read_int o map Symbol_Pos.symbol)
     (Scan.read Symbol_Pos.stopper scan_nat cs);
 
 in