--- a/src/Pure/Thy/thm_deps.ML Thu Sep 27 22:30:09 2001 +0200
+++ b/src/Pure/Thy/thm_deps.ML Fri Sep 28 11:04:44 2001 +0200
@@ -31,9 +31,9 @@
fun make_deps_graph (p, AbsP (_, _, prf)) = make_deps_graph (p, prf)
| make_deps_graph (p, Abst (_, _, prf)) = make_deps_graph (p, prf)
- | make_deps_graph (p, prf1 % prf2) =
+ | make_deps_graph (p, prf1 %% prf2) =
make_deps_graph (make_deps_graph (p, prf1), prf2)
- | make_deps_graph (p, prf %% _) = make_deps_graph (p, prf)
+ | make_deps_graph (p, prf % _) = make_deps_graph (p, prf)
| make_deps_graph (p, MinProof prfs) = foldl make_deps_graph (p, prfs)
| make_deps_graph (p as (gra, parents), prf) =
let val ((name, tags), prf') = dest_thm_axm prf