src/ZF/OrderType.thy

--- a/src/ZF/OrderType.thy	Tue Mar 06 17:01:37 2012 +0000
+++ b/src/ZF/OrderType.thy	Thu Mar 08 16:43:29 2012 +0000
@@ -74,8 +74,7 @@
   The smaller ordinal is an initial segment of the larger *)
 lemma lt_pred_Memrel:
     "j<i ==> pred(i, j, Memrel(i)) = j"
-apply (unfold pred_def lt_def)
-apply (simp (no_asm_simp))
+apply (simp add: pred_def lt_def)
 apply (blast intro: Ord_trans)
 done