--- a/src/ZF/IMP/Equiv.ML Fri Oct 13 10:49:05 2000 +0200
+++ b/src/ZF/IMP/Equiv.ML Fri Oct 13 11:15:56 2000 +0200
@@ -53,11 +53,11 @@
(* comp *)
by (Fast_tac 1);
(* while *)
-by (etac (Gamma_bnd_mono RS lfp_Tarski RS ssubst) 1);
+by (etac (Gamma_bnd_mono RS lfp_unfold RS ssubst) 1);
by (asm_simp_tac (simpset() addsimps [Gamma_def, bexp1]) 1);
by (blast_tac (claset() addSIs [bexp1]@evalb_type_intrs) 1);
(* recursive case of while *)
-by (etac (Gamma_bnd_mono RS lfp_Tarski RS ssubst) 1);
+by (etac (Gamma_bnd_mono RS lfp_unfold RS ssubst) 1);
by (asm_full_simp_tac (simpset() addsimps [Gamma_def, bexp1]) 1);
by (blast_tac (claset() addSIs [bexp1]@evalb_type_intrs) 1);
val com1 = result();