diff -r 7cfe7b6d501a -r c2c6d560e7b2 src/Pure/Tools/proof_general.ML --- a/src/Pure/Tools/proof_general.ML Sat Mar 15 10:29:42 2014 +0100 +++ b/src/Pure/Tools/proof_general.ML Sat Mar 15 11:22:25 2014 +0100 @@ -391,7 +391,7 @@ let val prev_facts = Global_Theory.facts_of (Toplevel.theory_of state); val facts = Global_Theory.facts_of (Toplevel.theory_of state'); - val (names, deps) = get_thm_deps (maps #2 (Facts.dest_static [prev_facts] facts)); + val (names, deps) = get_thm_deps (maps #2 (Facts.dest_static true [prev_facts] facts)); in if null names orelse null deps then () else thm_deps_message (spaces_quote names, spaces_quote deps)