# HG changeset patch
# User wenzelm
# Date 889456472 -3600
# Node ID c9033f4e0cd0536ecaa3320a6ea4b5e6ab030c94
# Parent  f710177068873b809ad7df77287b84f7657eeb26
Symbol.is_*;

diff -r f71017706887 -r c9033f4e0cd0 src/Pure/Thy/browser_info.ML
--- 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;