# HG changeset patch
# User wenzelm
# Date 889456401 -3600
# Node ID 4fce39cc7136d790f23227c52752297a07dbca1a
# Parent  a50ab39756db5652b0c45d9a4ccbebb8928fd195
Symbol.input;

diff -r a50ab39756db -r 4fce39cc7136 src/Pure/Thy/use.ML
--- a/src/Pure/Thy/use.ML	Mon Mar 09 16:12:39 1998 +0100
+++ b/src/Pure/Thy/use.ML	Mon Mar 09 16:13:21 1998 +0100
@@ -39,7 +39,7 @@
     fn name =>
       let
         val txt = File.read name;
-        val txt_out = implode (SymbolFont.write_charnames' (explode txt));
+        val txt_out = Symbol.input txt;
       in
         if txt = txt_out then use_orig name
         else