src/Pure/Thy/thm_deps.ML
changeset 11612 ae8450657bf0
parent 11543 d61b913431c5
child 11819 9283b3c11234
--- 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