Symbol.input;
authorwenzelm
Mon, 09 Mar 1998 16:13:21 +0100
changeset 4704 4fce39cc7136
parent 4703 a50ab39756db
child 4705 f71017706887
Symbol.input;
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