author | berghofe |
Wed, 06 Aug 1997 00:29:02 +0200 | |
changeset 3605 | d372fb6ec393 |
parent 3604 | 6bf9f09f3d61 |
child 3606 | 5d7073700fbc |
--- a/src/Pure/Thy/symbol_input.ML Wed Aug 06 00:26:19 1997 +0200 +++ b/src/Pure/Thy/symbol_input.ML Wed Aug 06 00:29:02 1997 +0200 @@ -13,8 +13,6 @@ structure SymbolInput: SYMBOL_INPUT = struct -fun file_exists name = file_info name <> ""; - fun fix_name name = if file_exists name then name else if file_exists (name ^ ".ML") then name ^ ".ML"