--- a/src/ZF/AC/rel_is_fun.ML Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/AC/rel_is_fun.ML Wed Jan 08 15:04:27 1997 +0100
@@ -20,8 +20,8 @@
by (etac domainE 1);
by (forward_tac [inj_is_fun RS apply_type] 1 THEN (atac 1));
by (rtac LeastI2 1);
-by (REPEAT (fast_tac (!claset addIs [fst_conv, left_inverse RS ssubst]
- addSEs [nat_into_Ord RS Ord_in_Ord]) 1));
+by (REPEAT (fast_tac (!claset addSEs [nat_into_Ord RS Ord_in_Ord]
+ addss (!simpset addsimps [left_inverse])) 1));
val lepoll_m_imp_domain_lepoll_m = result();
goalw Cardinal.thy [function_def]