diff -r bc1fb6941b54 -r 3cd767f8d78b src/ZF/Constructible/Wellorderings.thy
--- a/src/ZF/Constructible/Wellorderings.thy	Thu Jul 11 17:56:28 2002 +0200
+++ b/src/ZF/Constructible/Wellorderings.thy	Fri Jul 12 11:24:40 2002 +0200
@@ -161,9 +161,7 @@
 lemma (in M_axioms) order_isomorphism_abs [simp]: 
      "[| M(A); M(B); M(f) |] 
       ==> order_isomorphism(M,A,r,B,s,f) <-> f \<in> ord_iso(A,r,B,s)"
-by (simp add: typed_apply_abs [OF bij_is_fun] apply_closed 
-              order_isomorphism_def ord_iso_def)
-
+by (simp add: apply_closed order_isomorphism_def ord_iso_def)
 
 lemma (in M_axioms) pred_set_abs [simp]: 
      "[| M(r); M(B) |] ==> pred_set(M,A,x,r,B) <-> B = Order.pred(A,x,r)"
@@ -236,7 +234,7 @@
 apply (elim conjE CollectE) 
 apply (erule wellfounded_on_induct, assumption+)
  apply (insert well_ord_iso_separation [of A f r])
- apply (simp add: typed_apply_abs [OF bij_is_fun] apply_closed, clarify) 
+ apply (simp, clarify) 
 apply (drule_tac a = x in bij_is_fun [THEN apply_type], assumption, blast)
 done