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