src/Tools/WWW_Find/unicode_symbols.ML

 
 end;
 
 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;
 val symbol = Scan.one is_symbol >> (fn t => (str_of_token t, pos_of_token t));
 val name = Scan.one is_name >> str_of_token;

 val abbr = Scan.option ($$$ "abbrev" -- $$$ ":"
                         |-- (ascii_sym || $$$ ":" || name));
 
 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"]
   |> map Path.explode
   |> Path.appends;