src/ZF/ex/Limit.ML

--- a/src/ZF/ex/Limit.ML	Tue Apr 23 17:11:23 1996 +0200
+++ b/src/ZF/ex/Limit.ML	Tue Apr 23 17:11:44 1996 +0200
@@ -2167,9 +2167,9 @@
      add_type::nat_into_Ord::prems)) 1);
 by (etac lt_asym 1);
 by (assume_tac 1);
+by (asm_full_simp_tac (ZF_ss addsimps add_succ_right::succ_le_iff::prems) 1);
 by (asm_full_simp_tac (ZF_ss addsimps 
-    (succ_le_iff::add_succ::add_succ_right::le_iff::
-     add_type::nat_into_Ord::prems)) 1);
+    (add_succ::le_iff::add_type::nat_into_Ord::prems)) 1);
 by (safe_tac lemmas_cs);
 by (etac lt_irrefl 1);
 val add_le_elim1 = result();