--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Tue Sep 02 22:41:36 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Tue Sep 02 23:27:44 2008 +0200
@@ -177,7 +177,9 @@
fun setup_present_hook () = Toplevel.add_hook (fn _ => fn state => fn (state', opt_err) =>
if print_mode_active thm_depsN andalso Toplevel.is_theory state' andalso is_none opt_err then
- let val (names, deps) = ProofGeneralPgip.new_thms_deps state state' in
+ let val (names, deps) =
+ ProofGeneralPgip.new_thms_deps (Toplevel.theory_of state) (Toplevel.theory_of state')
+ in
if null names orelse null deps then ()
else thm_deps_message (spaces_quote names, spaces_quote deps)
end