diff -r 8de262a22f23 -r 2124b24454dd src/HOL/Lambda/Eta.thy
--- a/src/HOL/Lambda/Eta.thy	Fri Nov 25 18:58:43 2005 +0100
+++ b/src/HOL/Lambda/Eta.thy	Fri Nov 25 19:09:44 2005 +0100
@@ -67,16 +67,16 @@
   apply (simp add: diff_Suc subst_Var split: nat.split)
   done
 
-lemma free_eta: "s -e> t ==> (!!i. free t i = free s i)"
-  by (induct set: eta) (simp_all cong: conj_cong)
+lemma free_eta: "s -e> t ==> free t i = free s i"
+  by (induct fixing: i set: eta) (simp_all cong: conj_cong)
 
 lemma not_free_eta:
     "[| s -e> t; \<not> free s i |] ==> \<not> free t i"
   by (simp add: free_eta)
 
 lemma eta_subst [simp]:
-    "s -e> t ==> (!!u i. s[u/i] -e> t[u/i])"
-  by (induct set: eta) (simp_all add: subst_subst [symmetric])
+    "s -e> t ==> s[u/i] -e> t[u/i]"
+  by (induct fixing: u i set: eta) (simp_all add: subst_subst [symmetric])
 
 theorem lift_subst_dummy: "\<not> free s i \<Longrightarrow> lift (s[dummy/i]) i = s"
   by (induct s fixing: i dummy) simp_all
@@ -122,17 +122,17 @@
 subsection "Commutation of beta and eta"
 
 lemma free_beta:
-    "s -> t ==> (!!i. free t i \<Longrightarrow> free s i)"
-  by (induct set: beta) auto
+    "s -> t ==> free t i \<Longrightarrow> free s i"
+  by (induct fixing: i set: beta) auto
 
-lemma beta_subst [intro]: "s -> t ==> (!!u i. s[u/i] -> t[u/i])"
-  by (induct set: beta) (simp_all add: subst_subst [symmetric])
+lemma beta_subst [intro]: "s -> t ==> s[u/i] -> t[u/i]"
+  by (induct fixing: u i set: beta) (simp_all add: subst_subst [symmetric])
 
 lemma subst_Var_Suc [simp]: "t[Var i/i] = t[Var(i)/i + 1]"
   by (induct t fixing: i) (auto elim!: linorder_neqE simp: subst_Var)
 
-lemma eta_lift [simp]: "s -e> t ==> (!!i. lift s i -e> lift t i)"
-  by (induct set: eta) simp_all
+lemma eta_lift [simp]: "s -e> t ==> lift s i -e> lift t i"
+  by (induct fixing: i set: eta) simp_all
 
 lemma rtrancl_eta_subst: "s -e> t \<Longrightarrow> u[s/i] -e>> u[t/i]"
   apply (induct u fixing: s t i)