Symbol.is_*;

--- a/src/Pure/Thy/browser_info.ML	Mon Mar 09 16:14:15 1998 +0100
+++ b/src/Pure/Thy/browser_info.ML	Mon Mar 09 16:14:32 1998 +0100
@@ -289,10 +289,10 @@
         val (ancestors, body) =
           let
             fun make_links l result =
-              let val (pre, letter) = take_prefix (not o is_letter) l;
+              let val (pre, letter) = take_prefix (not o Symbol.is_letter) l;
 
                   val (id, rest) =
-                    take_prefix (is_quasi_letter orf is_digit) letter;
+                    take_prefix (Symbol.is_quasi_letter orf Symbol.is_digit) letter;
 
                   val id = implode id;