src/Pure/Thy/thm_deps.ML
changeset 32726 a900d3cd47cc
parent 31177 c39994cb152a
child 32810 f3466a5645fa
     1.1 --- a/src/Pure/Thy/thm_deps.ML	Mon Sep 28 12:09:55 2009 +0200
     1.2 +++ b/src/Pure/Thy/thm_deps.ML	Mon Sep 28 20:52:05 2009 +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 o #2) (map Thm.proof_body_of thms) [];
     1.9    in Present.display_graph (sort_wrt #ID deps) end;
    1.10  
    1.11  
    1.12 @@ -56,7 +56,7 @@
    1.13        |> sort_distinct (string_ord o pairself #1);
    1.14  
    1.15      val tab = Proofterm.fold_body_thms
    1.16 -      (fn (name, prop, _) => name <> "" ? Symtab.insert_list (op =) (name, prop))
    1.17 +      (fn (_, (name, prop, _)) => name <> "" ? Symtab.insert_list (op =) (name, prop))
    1.18        (map (Proofterm.strip_thm o Thm.proof_body_of o snd) thms) Symtab.empty;
    1.19      fun is_unused (name, th) =
    1.20        not (member (op aconv) (Symtab.lookup_list tab name) (Thm.prop_of th));