--- a/src/ZF/AC/WO6_WO1.ML Tue Jan 23 11:27:29 1996 +0100
+++ b/src/ZF/AC/WO6_WO1.ML Tue Jan 23 11:33:46 1996 +0100
@@ -83,7 +83,7 @@
(* ********************************************************************** *)
goalw thy [vv1_def] "vv1(f,m,b) <= f`b";
-by (rtac (letI RS letI) 1);
+by (rtac (LetI RS LetI) 1);
by (split_tac [expand_if] 1);
by (simp_tac (ZF_ss addsimps [domain_uu_subset]) 1);
val vv1_subset = result();
--- a/src/ZF/Let.ML Tue Jan 23 11:27:29 1996 +0100
+++ b/src/ZF/Let.ML Tue Jan 23 11:33:46 1996 +0100
@@ -11,4 +11,4 @@
val [prem] = goalw thy
[Let_def] "(!!x. x=t ==> P(u(x))) ==> P(let x=t in u(x))";
br (refl RS prem) 1;
-qed "letI";
+qed "LetI";