diff -r 70b789956bd3 -r 5e00a676a211 src/ZF/WF.ML
--- a/src/ZF/WF.ML Tue Jul 26 13:21:20 1994 +0200
+++ b/src/ZF/WF.ML Tue Jul 26 13:44:42 1994 +0200
@@ -95,7 +95,7 @@
rename_last_tac a ["1"] (i+1),
ares_tac prems i];
-(*The form of this rule is designed to match wfI2*)
+(*The form of this rule is designed to match wfI*)
val wfr::amem::prems = goal WF.thy
"[| wf(r); a:A; field(r)<=A; \
\ !!x.[| x: A; ALL y. : r --> P(y) |] ==> P(x) \
@@ -133,7 +133,7 @@
\ ==> wf(r)";
by (rtac ([wf_onI2, subs] MRS (wf_on_subset_A RS wf_on_field_imp_wf)) 1);
by (REPEAT (ares_tac [indhyp] 1));
-val wfI2 = result();
+val wfI = result();
(*** Properties of well-founded relations ***)