src/Pure/Thy/thm_deps.ML
changeset 21646 c07b5b0e8492
parent 20854 f9cf9e62d11c
child 21858 05f57309170c
     1.1 --- a/src/Pure/Thy/thm_deps.ML	Tue Dec 05 00:29:19 2006 +0100
     1.2 +++ b/src/Pure/Thy/thm_deps.ML	Tue Dec 05 00:30:38 2006 +0100
     1.3 @@ -25,9 +25,9 @@
     1.4  fun enable () = if ! proofs = 0 then proofs := 1 else ();
     1.5  fun disable () = proofs := 0;
     1.6  
     1.7 -fun dest_thm_axm (PThm (nt, prf, _, _)) = (nt, prf)
     1.8 -  | dest_thm_axm (PAxm (n, _, _)) = ((n ^ " (Ax)", []), MinProof ([], [], []))
     1.9 -  | dest_thm_axm _ = (("", []), MinProof ([], [], []));
    1.10 +fun dest_thm_axm (PThm (name, prf, _, _)) = (name, prf)
    1.11 +  | dest_thm_axm (PAxm (name, _, _)) = (name ^ " (Ax)", MinProof ([], [], []))
    1.12 +  | dest_thm_axm _ = ("", MinProof ([], [], []));
    1.13  
    1.14  fun make_deps_graph (AbsP (_, _, prf)) = make_deps_graph prf
    1.15    | make_deps_graph (Abst (_, _, prf)) = make_deps_graph prf
    1.16 @@ -37,9 +37,9 @@
    1.17        fold (make_deps_graph o Proofterm.proof_of_min_thm) thms #>
    1.18        fold (make_deps_graph o Proofterm.proof_of_min_axm) axms
    1.19    | make_deps_graph prf = (fn p as (gra, parents) =>
    1.20 -      let val ((name, tags), prf') = dest_thm_axm prf
    1.21 +      let val (name, prf') = dest_thm_axm prf
    1.22        in
    1.23 -        if name <> "" andalso not (PureThy.has_internal tags) then
    1.24 +        if name <> "" then
    1.25            if not (Symtab.defined gra name) then
    1.26              let
    1.27                val (gra', parents') = make_deps_graph prf' (gra, []);