diff -r 3294f727e20d -r b9f6154427a4 src/ZF/Epsilon.thy
--- a/src/ZF/Epsilon.thy	Thu Jan 23 09:16:53 2003 +0100
+++ b/src/ZF/Epsilon.thy	Thu Jan 23 10:30:14 2003 +0100
@@ -180,7 +180,7 @@
 lemma transrec_type:
     "[| !!x u. [| x:eclose({a});  u: Pi(x,B) |] ==> H(x,u) : B(x) |]
      ==> transrec(a,H) : B(a)"
-apply (rule_tac i = "a" in arg_in_eclose_sing [THEN eclose_induct])
+apply (rule_tac i = a in arg_in_eclose_sing [THEN eclose_induct])
 apply (subst transrec)
 apply (simp add: lam_type) 
 done
@@ -220,7 +220,7 @@
 by (subst rank_def [THEN def_transrec], simp)
 
 lemma Ord_rank [simp]: "Ord(rank(a))"
-apply (rule_tac a="a" in eps_induct) 
+apply (rule_tac a=a in eps_induct) 
 apply (subst rank)
 apply (rule Ord_succ [THEN Ord_UN])
 apply (erule bspec, assumption)
@@ -233,7 +233,7 @@
 done
 
 lemma rank_lt: "a:b ==> rank(a) < rank(b)"
-apply (rule_tac a1 = "b" in rank [THEN ssubst])
+apply (rule_tac a1 = b in rank [THEN ssubst])
 apply (erule UN_I [THEN ltI])
 apply (rule_tac [2] Ord_UN, auto)
 done