src/Pure/Thy/thm_deps.ML

--- a/src/Pure/Thy/thm_deps.ML	Sat Aug 20 15:52:29 2011 +0200
+++ b/src/Pure/Thy/thm_deps.ML	Sat Aug 20 16:06:27 2011 +0200
@@ -40,7 +40,7 @@
                path = "",
                parents = parents};
           in cons entry end;
-    val deps = Proofterm.fold_body_thms add_dep (map Thm.proof_body_of thms) [];
+    val deps = Proofterm.fold_body_thms add_dep (Future.joins (map Thm.future_body_of thms)) [];
   in Present.display_graph (sort_wrt #ID deps) end;
 
 
@@ -66,7 +66,8 @@
     val used =
       Proofterm.fold_body_thms
         (fn (a, _, _) => a <> "" ? Symtab.update (a, ()))
-        (map (Proofterm.strip_thm o Thm.proof_body_of o #1 o #2) new_thms) Symtab.empty;
+        (map Proofterm.strip_thm (Future.joins (map (Thm.future_body_of o #1 o #2) new_thms)))
+        Symtab.empty;
 
     fun is_unused a = not (Symtab.defined used a);