src/Tools/WWW_Find/unicode_symbols.ML
changeset 36960 01594f816e3a
parent 36692 54b64d4ad524
child 40527 e0c000e40c05
--- a/src/Tools/WWW_Find/unicode_symbols.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/Tools/WWW_Find/unicode_symbols.ML	Mon May 17 23:54:15 2010 +0200
@@ -114,8 +114,6 @@
 
 local (* Parser *)
 
-structure P = OuterParse;
-
 fun $$$ kw = Scan.one (is_keyword kw) >> str_of_token;
 val hex_code = Scan.one is_hex_code >> int_of_code;
 val ascii_sym = Scan.one is_ascii_sym >> str_of_token;
@@ -129,7 +127,7 @@
 
 in
 
-val line = (symbol -- unicode --| font -- abbr) >> P.triple1;
+val line = (symbol -- unicode --| font -- abbr) >> Parse.triple1;
 
 val symbols_path =
   [getenv "ISABELLE_HOME", "etc", "symbols"]