| changeset 37949 | 48a874444164 |
| parent 37873 | 66d90b2b87bc |
| child 37954 | a2e73df0b1e0 |
--- a/src/Pure/pure_setup.ML Fri Jul 23 18:42:46 2010 +0200 +++ b/src/Pure/pure_setup.ML Sat Jul 24 12:14:53 2010 +0200 @@ -51,7 +51,8 @@ (* ML toplevel use commands *) -fun use name = Toplevel.program (fn () => Thy_Info.use name); +fun use name = Toplevel.program (fn () => Thy_Load.use_ml (Path.explode name)); + fun use_thys name = Toplevel.program (fn () => Thy_Info.use_thys name); fun use_thy name = Toplevel.program (fn () => Thy_Info.use_thy name);