# HG changeset patch
# User wenzelm
# Date 1289675212 -3600
# Node ID e0c000e40c056fe09ca2a29eaf161018ab712a61
# Parent  ca3c6b1bfcdb9ce490719e0decf06aab51a3d561
qualified Symbol_Pos.symbol;

diff -r ca3c6b1bfcdb -r e0c000e40c05 src/Tools/WWW_Find/unicode_symbols.ML
--- a/src/Tools/WWW_Find/unicode_symbols.ML	Sat Nov 13 19:55:45 2010 +0100
+++ b/src/Tools/WWW_Find/unicode_symbols.ML	Sat Nov 13 20:06:52 2010 +0100
@@ -66,7 +66,7 @@
 
 fun end_position_of (Token (_, _, (_, epos))) = epos;
 
-val is_space = symbol #> (fn s => Symbol.is_blank s andalso s <> "\n");
+val is_space = Symbol_Pos.symbol #> (fn s => Symbol.is_blank s andalso s <> "\n");
 val scan_space =
   (Scan.many1 is_space @@@ Scan.optional ($$$ "\n") []
    ||
@@ -78,11 +78,11 @@
   ((fn x => Symbol.is_ascii x andalso
       not (Symbol.is_ascii_letter x
            orelse Symbol.is_ascii_digit x
-           orelse Symbol.is_ascii_blank x)) o symbol)
-  -- Scan.many (not o Symbol.is_ascii_blank o symbol)
+           orelse Symbol.is_ascii_blank x)) o Symbol_Pos.symbol)
+  -- Scan.many (not o Symbol.is_ascii_blank o Symbol_Pos.symbol)
   >> (token AsciiSymbol o op ::);
 
-fun not_contains xs c = not (member (op =) (explode xs) (symbol c));
+fun not_contains xs c = not (member (op =) (explode xs) (Symbol_Pos.symbol c));
 val scan_comment =
   $$$ "#" |-- (Scan.many (not_contains "\n") @@@ ($$$ "\n"))
   >> token Comment;
@@ -90,7 +90,7 @@
 fun tokenize syms =
   let
     val scanner =
-      Scan.one (Symbol.is_symbolic o symbol) >> (token Symbol o single) ||
+      Scan.one (Symbol.is_symbolic o Symbol_Pos.symbol) >> (token Symbol o single) ||
       scan_comment ||
       scan_space ||
       scan_code ||