changeset 38757 | 2b3e054ae6fc |
parent 38133 | 987680d2e77d |
child 40625 | 2d9222a2239d |
--- a/src/Pure/Thy/thy_load.ML Thu Aug 26 13:09:12 2010 +0200 +++ b/src/Pure/Thy/thy_load.ML Thu Aug 26 15:48:08 2010 +0200 @@ -195,7 +195,7 @@ val _ = Context.>> Local_Theory.propagate_ml_env; val provide = provide (src_path, (path, id)); - val _ = Context.>> (Context.mapping provide (Local_Theory.theory provide)); + val _ = Context.>> (Context.mapping provide (Local_Theory.background_theory provide)); in () end; fun exec_ml src_path = ML_Context.exec (fn () => use_ml src_path);