diff -r d07959fabde6 -r 2b3e054ae6fc src/Pure/Thy/thy_load.ML
--- 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);