src/Pure/ProofGeneral/proof_general_emacs.ML

   emacs_notify ("Proof General, theorem dependencies of " ^ thms ^ " are " ^ deps);
 
 in
 
 fun setup_present_hook () = Toplevel.add_hook (fn _ => fn state => fn state' =>
-  if print_mode_active thm_depsN andalso Toplevel.is_theory state' then
+  if print_mode_active thm_depsN andalso
+    can Toplevel.theory_of state andalso Toplevel.is_theory state'
+  then
     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)