src/Pure/Thy/thm_deps.ML
changeset 44331 aa9c1e9ef2ce
parent 42473 aca720fb3936
child 44333 cc53ce50f738
     1.1 --- a/src/Pure/Thy/thm_deps.ML	Sat Aug 20 15:52:29 2011 +0200
     1.2 +++ b/src/Pure/Thy/thm_deps.ML	Sat Aug 20 16:06:27 2011 +0200
     1.3 @@ -40,7 +40,7 @@
     1.4                 path = "",
     1.5                 parents = parents};
     1.6            in cons entry end;
     1.7 -    val deps = Proofterm.fold_body_thms add_dep (map Thm.proof_body_of thms) [];
     1.8 +    val deps = Proofterm.fold_body_thms add_dep (Future.joins (map Thm.future_body_of thms)) [];
     1.9    in Present.display_graph (sort_wrt #ID deps) end;
    1.10  
    1.11  
    1.12 @@ -66,7 +66,8 @@
    1.13      val used =
    1.14        Proofterm.fold_body_thms
    1.15          (fn (a, _, _) => a <> "" ? Symtab.update (a, ()))
    1.16 -        (map (Proofterm.strip_thm o Thm.proof_body_of o #1 o #2) new_thms) Symtab.empty;
    1.17 +        (map Proofterm.strip_thm (Future.joins (map (Thm.future_body_of o #1 o #2) new_thms)))
    1.18 +        Symtab.empty;
    1.19  
    1.20      fun is_unused a = not (Symtab.defined used a);
    1.21