diff -r 4af699cdfe47 -r c07b5b0e8492 src/Pure/Thy/thm_deps.ML --- a/src/Pure/Thy/thm_deps.ML Tue Dec 05 00:29:19 2006 +0100 +++ b/src/Pure/Thy/thm_deps.ML Tue Dec 05 00:30:38 2006 +0100 @@ -25,9 +25,9 @@ fun enable () = if ! proofs = 0 then proofs := 1 else (); fun disable () = proofs := 0; -fun dest_thm_axm (PThm (nt, prf, _, _)) = (nt, prf) - | dest_thm_axm (PAxm (n, _, _)) = ((n ^ " (Ax)", []), MinProof ([], [], [])) - | dest_thm_axm _ = (("", []), MinProof ([], [], [])); +fun dest_thm_axm (PThm (name, prf, _, _)) = (name, prf) + | dest_thm_axm (PAxm (name, _, _)) = (name ^ " (Ax)", MinProof ([], [], [])) + | dest_thm_axm _ = ("", MinProof ([], [], [])); fun make_deps_graph (AbsP (_, _, prf)) = make_deps_graph prf | make_deps_graph (Abst (_, _, prf)) = make_deps_graph prf @@ -37,9 +37,9 @@ fold (make_deps_graph o Proofterm.proof_of_min_thm) thms #> fold (make_deps_graph o Proofterm.proof_of_min_axm) axms | make_deps_graph prf = (fn p as (gra, parents) => - let val ((name, tags), prf') = dest_thm_axm prf + let val (name, prf') = dest_thm_axm prf in - if name <> "" andalso not (PureThy.has_internal tags) then + if name <> "" then if not (Symtab.defined gra name) then let val (gra', parents') = make_deps_graph prf' (gra, []);