author | wenzelm |
Mon, 25 May 1998 21:28:07 +0200 | |
changeset 4966 | 47b8f2d12c53 |
parent 4965 | 06914837e073 |
child 4967 | c9c481bc0216 |
--- a/src/Pure/Thy/thy_read.ML Mon May 25 21:27:22 1998 +0200 +++ b/src/Pure/Thy/thy_read.ML Mon May 25 21:28:07 1998 +0200 @@ -267,8 +267,7 @@ Use.use ml_file); (*Store theory again because it could have been redefined*) - use_strings - ["val _ = store_theory (" ^ tname ^ ".thy, " ^ quote tname ^ ");"]; + use_strings ["val _ = store_theory " ^ tname ^ ".thy;"]; (*Add theory to list of all loaded theories (for index.html) and add it to its parents' sub-charts*)