src/Pure/Tools/proof_general.ML

   if ! thm_deps andalso can Toplevel.theory_of state andalso Toplevel.is_theory state'
   then
     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)
     end
   else ());