src/Pure/Thy/thm_deps.ML
changeset 11612 ae8450657bf0
parent 11543 d61b913431c5
child 11819 9283b3c11234
     1.1 --- a/src/Pure/Thy/thm_deps.ML	Thu Sep 27 22:30:09 2001 +0200
     1.2 +++ b/src/Pure/Thy/thm_deps.ML	Fri Sep 28 11:04:44 2001 +0200
     1.3 @@ -31,9 +31,9 @@
     1.4  
     1.5  fun make_deps_graph (p, AbsP (_, _, prf)) = make_deps_graph (p, prf)
     1.6    | make_deps_graph (p, Abst (_, _, prf)) = make_deps_graph (p, prf)
     1.7 -  | make_deps_graph (p, prf1 % prf2) =
     1.8 +  | make_deps_graph (p, prf1 %% prf2) =
     1.9        make_deps_graph (make_deps_graph (p, prf1), prf2)
    1.10 -  | make_deps_graph (p, prf %% _) = make_deps_graph (p, prf)
    1.11 +  | make_deps_graph (p, prf % _) = make_deps_graph (p, prf)
    1.12    | make_deps_graph (p, MinProof prfs) = foldl make_deps_graph (p, prfs)
    1.13    | make_deps_graph (p as (gra, parents), prf) =
    1.14        let val ((name, tags), prf') = dest_thm_axm prf