# HG changeset patch # User wenzelm # Date 1220434035 -7200 # Node ID 48b9c8756020d6839afa720fe59bc9eff111af8e # Parent 44054657ea5607f6d954088f8e5b772be020664d theorem dependency hook: check previous state; diff -r 44054657ea56 -r 48b9c8756020 src/Pure/ProofGeneral/proof_general_emacs.ML --- a/src/Pure/ProofGeneral/proof_general_emacs.ML Wed Sep 03 11:26:59 2008 +0200 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Wed Sep 03 11:27:15 2008 +0200 @@ -176,7 +176,9 @@ 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