# HG changeset patch
# User wenzelm
# Date 876500611 -7200
# Node ID e0baea4d485a5866155f01b630ffbd86501bac10
# Parent  56544d061e1d1910d9631de593e2682f1be5d1ed
fixed dots;

diff -r 56544d061e1d -r e0baea4d485a src/ZF/AC.ML
--- a/src/ZF/AC.ML	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/AC.ML	Fri Oct 10 18:23:31 1997 +0200
@@ -25,7 +25,7 @@
 qed "AC_ball_Pi";
 
 goal AC.thy "EX f. f: (PROD X: Pow(C)-{0}. X)";
-by (res_inst_tac [("B1", "%x.x")] (AC_Pi RS exE) 1);
+by (res_inst_tac [("B1", "%x. x")] (AC_Pi RS exE) 1);
 by (etac exI 2);
 by (Blast_tac 1);
 qed "AC_Pi_Pow";
@@ -33,7 +33,7 @@
 val [nonempty] = goal AC.thy
      "[| !!x. x:A ==> (EX y. y:x)       \
 \     |] ==> EX f: A->Union(A). ALL x:A. f`x : x";
-by (res_inst_tac [("B1", "%x.x")] (AC_Pi RS exE) 1);
+by (res_inst_tac [("B1", "%x. x")] (AC_Pi RS exE) 1);
 by (etac nonempty 1);
 by (blast_tac (!claset addDs [apply_type] addIs [Pi_type]) 1);
 qed "AC_func";
diff -r 56544d061e1d -r e0baea4d485a src/ZF/AC/AC18_AC19.ML
--- a/src/ZF/AC/AC18_AC19.ML	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/AC/AC18_AC19.ML	Fri Oct 10 18:23:31 1997 +0200
@@ -47,7 +47,7 @@
 
 val [prem] = goalw thy [AC18_def, AC19_def] "AC18 ==> AC19";
 by (rtac allI 1);
-by (res_inst_tac [("B1","%x.x")] (forall_elim_vars 0 prem RS revcut_rl) 1);
+by (res_inst_tac [("B1","%x. x")] (forall_elim_vars 0 prem RS revcut_rl) 1);
 by (Fast_tac 1);
 qed "AC18_AC19";
 
diff -r 56544d061e1d -r e0baea4d485a src/ZF/AC/Cardinal_aux.ML
--- a/src/ZF/AC/Cardinal_aux.ML	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/AC/Cardinal_aux.ML	Fri Oct 10 18:23:31 1997 +0200
@@ -187,7 +187,7 @@
 
 goalw thy [eqpoll_def] "!!A B. A Int B = 0 ==> A Un B eqpoll A + B";
 by (res_inst_tac [("x","lam a:A Un B. if(a:A,Inl(a),Inr(a))")] exI 1);
-by (res_inst_tac [("d","%z. case(%x.x, %x.x, z)")] lam_bijective 1);
+by (res_inst_tac [("d","%z. case(%x. x, %x. x, z)")] lam_bijective 1);
 by (fast_tac (!claset addSIs [if_type, InlI, InrI]) 1);
 by (TRYALL (etac sumE ));
 by (TRYALL (split_tac [expand_if]));
diff -r 56544d061e1d -r e0baea4d485a src/ZF/AC/WO6_WO1.ML
--- a/src/ZF/AC/WO6_WO1.ML	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/AC/WO6_WO1.ML	Fri Oct 10 18:23:31 1997 +0200
@@ -244,7 +244,7 @@
     "!!a. [| ALL g<a. ALL d<a. domain(uu(f,b,g,d)) ~= 0 -->             \
 \            domain(uu(f,b,g,d)) eqpoll succ(m);                        \
 \            ALL b<a. f`b lepoll succ(m); y*y<=y;                       \
-\            (UN b<a.f`b)=y;  Ord(a);  m:nat;  s:f`b;  b<a              \
+\            (UN b<a. f`b)=y;  Ord(a);  m:nat;  s:f`b;  b<a              \
 \         |] ==> (UN g<a++a. gg2(f,a,b,s) ` g) = y";
 by (dtac sym 1);
 by (asm_simp_tac
diff -r 56544d061e1d -r e0baea4d485a src/ZF/Arith.ML
--- a/src/ZF/Arith.ML	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Arith.ML	Fri Oct 10 18:23:31 1997 +0200
@@ -489,7 +489,7 @@
 (*le monotonicity, 1st argument*)
 goal Arith.thy
     "!!i j k. [| i le j; j:nat; k:nat |] ==> i#+k le j#+k";
-by (res_inst_tac [("f", "%j.j#+k")] Ord_lt_mono_imp_le_mono 1);
+by (res_inst_tac [("f", "%j. j#+k")] Ord_lt_mono_imp_le_mono 1);
 by (REPEAT (ares_tac [add_lt_mono1, add_type RS nat_into_Ord] 1));
 qed "add_le_mono1";
 
diff -r 56544d061e1d -r e0baea4d485a src/ZF/Arith.thy
--- a/src/ZF/Arith.thy	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Arith.thy	Fri Oct 10 18:23:31 1997 +0200
@@ -18,8 +18,8 @@
 defs
     rec_def  "rec(k,a,b) ==  transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))"
 
-    add_def  "m#+n == rec(m, n, %u v.succ(v))"
-    diff_def "m#-n == rec(n, m, %u v. rec(v, 0, %x y.x))"
+    add_def  "m#+n == rec(m, n, %u v. succ(v))"
+    diff_def "m#-n == rec(n, m, %u v. rec(v, 0, %x y. x))"
     mult_def "m#*n == rec(m, 0, %u v. n #+ v)"
     mod_def  "m mod n == transrec(m, %j f. if(j<n, j, f`(j#-n)))"
     div_def  "m div n == transrec(m, %j f. if(j<n, 0, succ(f`(j#-n))))"
diff -r 56544d061e1d -r e0baea4d485a src/ZF/Cardinal.ML
--- a/src/ZF/Cardinal.ML	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Cardinal.ML	Fri Oct 10 18:23:31 1997 +0200
@@ -187,7 +187,7 @@
 (** LEAST -- the least number operator [from HOL/Univ.ML] **)
 
 val [premP,premOrd,premNot] = goalw Cardinal.thy [Least_def]
-    "[| P(i);  Ord(i);  !!x. x<i ==> ~P(x) |] ==> (LEAST x.P(x)) = i";
+    "[| P(i);  Ord(i);  !!x. x<i ==> ~P(x) |] ==> (LEAST x. P(x)) = i";
 by (rtac the_equality 1);
 by (blast_tac (!claset addSIs [premP,premOrd,premNot]) 1);
 by (REPEAT (etac conjE 1));
@@ -195,7 +195,7 @@
 by (ALLGOALS (blast_tac (!claset addSIs [premP] addSDs [premNot])));
 qed "Least_equality";
 
-goal Cardinal.thy "!!i. [| P(i);  Ord(i) |] ==> P(LEAST x.P(x))";
+goal Cardinal.thy "!!i. [| P(i);  Ord(i) |] ==> P(LEAST x. P(x))";
 by (etac rev_mp 1);
 by (trans_ind_tac "i" [] 1);
 by (rtac impI 1);
@@ -206,7 +206,7 @@
 qed "LeastI";
 
 (*Proof is almost identical to the one above!*)
-goal Cardinal.thy "!!i. [| P(i);  Ord(i) |] ==> (LEAST x.P(x)) le i";
+goal Cardinal.thy "!!i. [| P(i);  Ord(i) |] ==> (LEAST x. P(x)) le i";
 by (etac rev_mp 1);
 by (trans_ind_tac "i" [] 1);
 by (rtac impI 1);
@@ -217,7 +217,7 @@
 qed "Least_le";
 
 (*LEAST really is the smallest*)
-goal Cardinal.thy "!!i. [| P(i);  i < (LEAST x.P(x)) |] ==> Q";
+goal Cardinal.thy "!!i. [| P(i);  i < (LEAST x. P(x)) |] ==> Q";
 by (rtac (Least_le RSN (2,lt_trans2) RS lt_irrefl) 1);
 by (REPEAT (eresolve_tac [asm_rl, ltE] 1));
 qed "less_LeastE";
@@ -232,12 +232,12 @@
 
 (*If there is no such P then LEAST is vacuously 0*)
 goalw Cardinal.thy [Least_def]
-    "!!P. [| ~ (EX i. Ord(i) & P(i)) |] ==> (LEAST x.P(x)) = 0";
+    "!!P. [| ~ (EX i. Ord(i) & P(i)) |] ==> (LEAST x. P(x)) = 0";
 by (rtac the_0 1);
 by (Blast_tac 1);
 qed "Least_0";
 
-goal Cardinal.thy "Ord(LEAST x.P(x))";
+goal Cardinal.thy "Ord(LEAST x. P(x))";
 by (excluded_middle_tac "EX i. Ord(i) & P(i)" 1);
 by (safe_tac (!claset));
 by (rtac (Least_le RS ltE) 2);
@@ -251,7 +251,7 @@
 
 (*Not needed for simplification, but helpful below*)
 val prems = goal Cardinal.thy
-    "[| !!y. P(y) <-> Q(y) |] ==> (LEAST x.P(x)) = (LEAST x.Q(x))";
+    "[| !!y. P(y) <-> Q(y) |] ==> (LEAST x. P(x)) = (LEAST x. Q(x))";
 by (simp_tac (!simpset addsimps prems) 1);
 qed "Least_cong";
 
@@ -570,7 +570,7 @@
     "!!A B. [| A lepoll B;  b ~: B |] ==> cons(a,A) lepoll cons(b,B)";
 by (safe_tac (!claset));
 by (res_inst_tac [("x", "lam y: cons(a,A).if(y=a, b, f`y)")] exI 1);
-by (res_inst_tac [("d","%z.if(z:B, converse(f)`z, a)")] 
+by (res_inst_tac [("d","%z. if(z:B, converse(f)`z, a)")] 
     lam_injective 1);
 by (asm_simp_tac (!simpset addsimps [inj_is_fun RS apply_type, cons_iff]
                         setloop etac consE') 1);
diff -r 56544d061e1d -r e0baea4d485a src/ZF/CardinalArith.ML
--- a/src/ZF/CardinalArith.ML	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/CardinalArith.ML	Fri Oct 10 18:23:31 1997 +0200
@@ -103,8 +103,8 @@
 
 goalw CardinalArith.thy [eqpoll_def] "succ(A)+B eqpoll succ(A+B)";
 by (rtac exI 1);
-by (res_inst_tac [("c", "%z.if(z=Inl(A),A+B,z)"), 
-                  ("d", "%z.if(z=A+B,Inl(A),z)")] 
+by (res_inst_tac [("c", "%z. if(z=Inl(A),A+B,z)"), 
+                  ("d", "%z. if(z=A+B,Inl(A),z)")] 
     lam_bijective 1);
 by (ALLGOALS
     (asm_simp_tac (!simpset addsimps [succI2, mem_imp_not_eq]
@@ -269,7 +269,7 @@
 goalw CardinalArith.thy [eqpoll_def] "succ(A)*B eqpoll B + A*B";
 by (rtac exI 1);
 by (res_inst_tac [("c", "%<x,y>. if(x=A, Inl(y), Inr(<x,y>))"), 
-                  ("d", "case(%y. <A,y>, %z.z)")] 
+                  ("d", "case(%y. <A,y>, %z. z)")] 
     lam_bijective 1);
 by (safe_tac (!claset addSEs [sumE]));
 by (ALLGOALS
@@ -315,7 +315,7 @@
     "lam z:cons(u,A). if(z=u, f`0,      \
 \                        if(z: range(f), f`succ(converse(f)`z), z))")] exI 1);
 by (res_inst_tac [("d", "%y. if(y: range(f),    \
-\                               nat_case(u, %z.f`z, converse(f)`y), y)")] 
+\                               nat_case(u, %z. f`z, converse(f)`y), y)")] 
     lam_injective 1);
 by (fast_tac (!claset addSIs [if_type, nat_succI, apply_type]
                       addIs  [inj_is_fun, inj_converse_fun]) 1);
diff -r 56544d061e1d -r e0baea4d485a src/ZF/Coind/Map.ML
--- a/src/ZF/Coind/Map.ML	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Coind/Map.ML	Fri Oct 10 18:23:31 1997 +0200
@@ -18,7 +18,7 @@
 by (Fast_tac 1);
 qed "qbeta_emp";
 
-goal Map.thy "!!A.a ~: A ==> Sigma(A,B)``{a}=0";
+goal Map.thy "!!A. a ~: A ==> Sigma(A,B)``{a}=0";
 by (Fast_tac 1);
 qed "image_Sigma1";
 
@@ -44,7 +44,7 @@
 (* Theorems *)
 
 val prems = goalw Map.thy [PMap_def,TMap_def]
-  "[| m:PMap(A,quniv(B)); !!x.x:A ==> x:univ(B) |] ==> m:quniv(B)";
+  "[| m:PMap(A,quniv(B)); !!x. x:A ==> x:univ(B) |] ==> m:quniv(B)";
 by (cut_facts_tac prems 1);
 by (rtac (MapQU_lemma RS subsetD) 1);
 by (rtac subsetI 1);
@@ -56,7 +56,7 @@
 (* Monotonicity                                                 *)
 (* ############################################################ *)
 
-goalw Map.thy [PMap_def,TMap_def] "!!A.B<=C ==> PMap(A,B)<=PMap(A,C)";
+goalw Map.thy [PMap_def,TMap_def] "!!A. B<=C ==> PMap(A,B)<=PMap(A,C)";
 by (Fast_tac 1);
 qed "map_mono";
 
@@ -139,11 +139,11 @@
 
 (* Lemmas *)
 
-goal Map.thy  "domain(UN x:A.B(x)) = (UN x:A.domain(B(x)))";
+goal Map.thy  "domain(UN x:A. B(x)) = (UN x:A. domain(B(x)))";
 by (Fast_tac 1);
 qed "domain_UN";
 
-goal Map.thy  "domain(Sigma(A,B)) = {x:A.EX y.y:B(x)}";
+goal Map.thy  "domain(Sigma(A,B)) = {x:A. EX y. y:B(x)}";
 by (simp_tac (!simpset addsimps [domain_UN,domain_0,domain_cons]) 1);
 by (Fast_tac 1);
 qed "domain_Sigma";
@@ -155,7 +155,7 @@
 qed "map_domain_emp";
 
 goalw Map.thy [map_owr_def] 
-  "!!a.b ~= 0 ==> domain(map_owr(f,a,b)) = {a} Un domain(f)";
+  "!!a. b ~= 0 ==> domain(map_owr(f,a,b)) = {a} Un domain(f)";
 by (simp_tac (!simpset addsimps [domain_Sigma]) 1);
 by (rtac equalityI 1);
 by (Fast_tac 1);
@@ -179,7 +179,7 @@
 qed "map_app_owr1";
 
 goalw Map.thy [map_app_def,map_owr_def] 
-  "!!a.c ~= a ==> map_app(map_owr(f,a,b),c)= map_app(f,c)";
+  "!!a. c ~= a ==> map_app(map_owr(f,a,b),c)= map_app(f,c)";
 by (rtac (excluded_middle RS disjE) 1);
 by (stac qbeta_emp 1);
 by (assume_tac 1);
diff -r 56544d061e1d -r e0baea4d485a src/ZF/Coind/Map.thy
--- a/src/ZF/Coind/Map.thy	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Coind/Map.thy	Fri Oct 10 18:23:31 1997 +0200
@@ -10,7 +10,7 @@
   TMap :: [i,i] => i
   PMap :: [i,i] => i
 defs
-  TMap_def "TMap(A,B) == {m:Pow(A*Union(B)).ALL a:A.m``{a}:B}"
+  TMap_def "TMap(A,B) == {m:Pow(A*Union(B)).ALL a:A. m``{a}:B}"
   PMap_def "PMap(A,B) == TMap(A,cons(0,B))"
 
 (* Note: 0:B ==> TMap(A,B) = PMap(A,B) *)
diff -r 56544d061e1d -r e0baea4d485a src/ZF/Coind/Types.thy
--- a/src/ZF/Coind/Types.thy	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Coind/Types.thy	Fri Oct 10 18:23:31 1997 +0200
@@ -27,14 +27,14 @@
 defs
   te_rec_def
     "te_rec(te,c,h) ==   
-    Vrec(te,%te g.TyEnv_case(c,%tem x t.h(tem,x,t,g`tem),te))"
+    Vrec(te,%te g. TyEnv_case(c,%tem x t. h(tem,x,t,g`tem),te))"
   
 consts
   te_dom :: i => i
   te_app :: [i,i] => i
 defs
-  te_dom_def "te_dom(te) == te_rec(te,0,% te x t r.r Un {x})"
-  te_app_def "te_app(te,x) == te_rec(te,0, % te y t r.if(x=y,t,r))"
+  te_dom_def "te_dom(te) == te_rec(te,0,% te x t r. r Un {x})"
+  te_app_def "te_app(te,x) == te_rec(te,0, % te y t r. if(x=y,t,r))"
   
 
 end
diff -r 56544d061e1d -r e0baea4d485a src/ZF/Coind/Values.ML
--- a/src/ZF/Coind/Values.ML	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Coind/Values.ML	Fri Oct 10 18:23:31 1997 +0200
@@ -42,7 +42,7 @@
 
 (* Nonempty sets *)
 
-val prems = goal Values.thy "A ~= 0 ==> EX a.a:A";
+val prems = goal Values.thy "A ~= 0 ==> EX a. a:A";
 by (cut_facts_tac prems 1);
 by (rtac (foundation RS disjE) 1);
 by (Fast_tac 1);
@@ -60,7 +60,7 @@
 qed "v_closNE";
 
 goalw Values.thy (sum_def::QPair_def::QInl_def::QInr_def::Val_ValEnv.con_defs)
-  "!!c.c:Const ==> v_const(c) ~= 0";
+  "!!c. c:Const ==> v_const(c) ~= 0";
 by (dtac constNEE 1);
 by (etac not_emptyE 1);
 by (rtac not_emptyI 1);
@@ -75,7 +75,7 @@
 
 (* Proving that the empty set is not a value *)
 
-goal Values.thy "!!v.v:Val ==> v ~= 0";
+goal Values.thy "!!v. v:Val ==> v ~= 0";
 by (etac ValE 1);
 by (ALLGOALS hyp_subst_tac);
 by (etac v_constNE 1);
@@ -102,7 +102,7 @@
 qed "ve_app_owr1";
 
 goalw Values.thy [ve_app_def,ve_owr_def]
- "!!ve.ve:ValEnv ==> x ~= y ==> ve_app(ve_owr(ve,x,v),y) = ve_app(ve,y)";
+ "!!ve. ve:ValEnv ==> x ~= y ==> ve_app(ve_owr(ve,x,v),y) = ve_app(ve,y)";
 by (etac ValEnvE 1);
 by (asm_full_simp_tac (!simpset addsimps Val_ValEnv.case_eqns) 1);
 by (rtac map_app_owr2 1);
diff -r 56544d061e1d -r e0baea4d485a src/ZF/Coind/Values.thy
--- a/src/ZF/Coind/Values.thy	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Coind/Values.thy	Fri Oct 10 18:23:31 1997 +0200
@@ -27,11 +27,11 @@
   ve_emp_def "ve_emp == ve_mk(map_emp)"
   ve_owr_def
     "ve_owr(ve,x,v) ==   
-    ve_mk(Val_ValEnv_case(%x.0,%x y z.0,%m.map_owr(m,x,v),ve))"
+    ve_mk(Val_ValEnv_case(%x.0,%x y z.0,%m. map_owr(m,x,v),ve))"
   ve_dom_def
-    "ve_dom(ve) == Val_ValEnv_case(%x.0,%x y z.0,%m.domain(m),ve)"
+    "ve_dom(ve) == Val_ValEnv_case(%x.0,%x y z.0,%m. domain(m),ve)"
   ve_app_def
-    "ve_app(ve,a) == Val_ValEnv_case(%x.0,%x y z.0,%m.map_app(m,a),ve)"
+    "ve_app(ve,a) == Val_ValEnv_case(%x.0,%x y z.0,%m. map_app(m,a),ve)"
 
 end
 
diff -r 56544d061e1d -r e0baea4d485a src/ZF/EquivClass.ML
--- a/src/ZF/EquivClass.ML	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/EquivClass.ML	Fri Oct 10 18:23:31 1997 +0200
@@ -238,7 +238,7 @@
 (*Obsolete?*)
 val [equivA,ZinA,congt,commute] = goalw EquivClass.thy [quotient_def]
     "[| equiv(A,r);  Z: A/r;  \
-\       !!w. [| w: A |] ==> congruent(r, %z.b(w,z));    \
+\       !!w. [| w: A |] ==> congruent(r, %z. b(w,z));    \
 \       !!x y. [| x: A;  y: A |] ==> b(y,x) = b(x,y)    \
 \    |] ==> congruent(r, %w. UN z: Z. b(w,z))";
 val congt' = rewrite_rule [congruent_def] congt;
diff -r 56544d061e1d -r e0baea4d485a src/ZF/List.ML
--- a/src/ZF/List.ML	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/List.ML	Fri Oct 10 18:23:31 1997 +0200
@@ -265,13 +265,13 @@
 (*** theorems about map ***)
 
 val prems = goal List.thy
-    "l: list(A) ==> map(%u.u, l) = l";
+    "l: list(A) ==> map(%u. u, l) = l";
 by (list_ind_tac "l" prems 1);
 by (ALLGOALS Asm_simp_tac);
 qed "map_ident";
 
 val prems = goal List.thy
-    "l: list(A) ==> map(h, map(j,l)) = map(%u.h(j(u)), l)";
+    "l: list(A) ==> map(h, map(j,l)) = map(%u. h(j(u)), l)";
 by (list_ind_tac "l" prems 1);
 by (ALLGOALS Asm_simp_tac);
 qed "map_compose";
diff -r 56544d061e1d -r e0baea4d485a src/ZF/List.thy
--- a/src/ZF/List.thy	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/List.thy	Fri Oct 10 18:23:31 1997 +0200
@@ -31,16 +31,16 @@
 
 constdefs
   hd      :: i=>i
-  "hd(l)       == list_case(0, %x xs.x, l)"
+  "hd(l)       == list_case(0, %x xs. x, l)"
   
   tl      :: i=>i
-  "tl(l)       == list_case(Nil, %x xs.xs, l)"
+  "tl(l)       == list_case(Nil, %x xs. xs, l)"
   
   drop       :: [i,i]=>i
   "drop(i,l)   == rec(i, l, %j r. tl(r))"
 
   list_rec   :: [i, i, [i,i,i]=>i] => i
-  "list_rec(l,c,h) == Vrec(l, %l g.list_case(c, %x xs. h(x, xs, g`xs), l))"
+  "list_rec(l,c,h) == Vrec(l, %l g. list_case(c, %x xs. h(x, xs, g`xs), l))"
 
   map        :: [i=>i, i] => i
   "map(f,l)    == list_rec(l,  Nil,  %x xs r. Cons(f(x), r))"
diff -r 56544d061e1d -r e0baea4d485a src/ZF/OrdQuant.ML
--- a/src/ZF/OrdQuant.ML	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/OrdQuant.ML	Fri Oct 10 18:23:31 1997 +0200
@@ -49,7 +49,7 @@
 
 (*Not of the general form for such rules; ~EX has become ALL~ *)
 qed_goal "oexCI" thy 
-   "[| ALL x<A. ~P(x) ==> P(a);  a<A |] ==> EX x<A.P(x)"
+   "[| ALL x<A. ~P(x) ==> P(a);  a<A |] ==> EX x<A. P(x)"
  (fn prems=>
   [ (rtac classical 1),
     (REPEAT (ares_tac (prems@[oexI,oallI,notI,notE]) 1)) ]);
@@ -85,7 +85,7 @@
  (fn _=> [ (fast_tac (!claset addIs [OUN_I] addSEs [OUN_E]) 1) ]);
 
 qed_goal "OUN_cong" thy
-    "[| i=j;  !!x. x<j ==> C(x)=D(x) |] ==> (UN x<i.C(x)) = (UN x<j.D(x))"
+    "[| i=j;  !!x. x<j ==> C(x)=D(x) |] ==> (UN x<i. C(x)) = (UN x<j. D(x))"
  (fn prems=>
       [ rtac equality_iffI 1,
         simp_tac (!simpset addcongs [oex_cong] addsimps (OUN_iff::prems)) 1 ]);
diff -r 56544d061e1d -r e0baea4d485a src/ZF/OrderArith.ML
--- a/src/ZF/OrderArith.ML	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/OrderArith.ML	Fri Oct 10 18:23:31 1997 +0200
@@ -136,7 +136,7 @@
      ord_iso(A+B, radd(A,r,B,s), A Un B, r Un s) *)
 goal OrderArith.thy
     "!!A B. A Int B = 0 ==>     \
-\           (lam z:A+B. case(%x.x, %y.y, z)) : bij(A+B, A Un B)";
+\           (lam z:A+B. case(%x. x, %y. y, z)) : bij(A+B, A Un B)";
 by (res_inst_tac [("d", "%z. if(z:A, Inl(z), Inr(z))")] 
     lam_bijective 1);
 by (blast_tac (!claset addSIs [if_type]) 2);
@@ -149,15 +149,15 @@
 (** Associativity **)
 
 goal OrderArith.thy
- "(lam z:(A+B)+C. case(case(Inl, %y.Inr(Inl(y))), %y. Inr(Inr(y)), z)) \
+ "(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z)) \
 \ : bij((A+B)+C, A+(B+C))";
-by (res_inst_tac [("d", "case(%x.Inl(Inl(x)), case(%x.Inl(Inr(x)), Inr))")] 
+by (res_inst_tac [("d", "case(%x. Inl(Inl(x)), case(%x. Inl(Inr(x)), Inr))")] 
     lam_bijective 1);
 by (ALLGOALS (asm_simp_tac (!simpset setloop etac sumE)));
 qed "sum_assoc_bij";
 
 goal OrderArith.thy
- "(lam z:(A+B)+C. case(case(Inl, %y.Inr(Inl(y))), %y. Inr(Inr(y)), z)) \
+ "(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z)) \
 \ : ord_iso((A+B)+C, radd(A+B, radd(A,r,B,s), C, t),    \
 \           A+(B+C), radd(A, r, B+C, radd(B,s,C,t)))";
 by (resolve_tac [sum_assoc_bij RS ord_isoI] 1);
@@ -283,7 +283,7 @@
   case_cong, id_conv, comp_lam, case_case.*)
 goal OrderArith.thy
  "!!a. a~:C ==> \
-\      (lam x:C*B + D. case(%x.x, %y.<a,y>, x)) \
+\      (lam x:C*B + D. case(%x. x, %y.<a,y>, x)) \
 \      : bij(C*B + D, C*B Un {a}*D)";
 by (rtac subst_elem 1);
 by (resolve_tac [id_bij RS sum_bij RS comp_bij] 1);
@@ -298,7 +298,7 @@
 
 goal OrderArith.thy
  "!!A. [| a:A;  well_ord(A,r) |] ==> \
-\   (lam x:pred(A,a,r)*B + pred(B,b,s). case(%x.x, %y.<a,y>, x)) \
+\   (lam x:pred(A,a,r)*B + pred(B,b,s). case(%x. x, %y.<a,y>, x)) \
 \   : ord_iso(pred(A,a,r)*B + pred(B,b,s),              \
 \                 radd(A*B, rmult(A,r,B,s), B, s),      \
 \             pred(A,a,r)*B Un {a}*pred(B,b,s), rmult(A,r,B,s))";
@@ -314,7 +314,7 @@
 (** Distributive law **)
 
 goal OrderArith.thy
- "(lam <x,z>:(A+B)*C. case(%y.Inl(<y,z>), %y.Inr(<y,z>), x)) \
+ "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x)) \
 \ : bij((A+B)*C, (A*C)+(B*C))";
 by (res_inst_tac
     [("d", "case(%<x,y>.<Inl(x),y>, %<x,y>.<Inr(x),y>)")] lam_bijective 1);
@@ -323,7 +323,7 @@
 qed "sum_prod_distrib_bij";
 
 goal OrderArith.thy
- "(lam <x,z>:(A+B)*C. case(%y.Inl(<y,z>), %y.Inr(<y,z>), x)) \
+ "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x)) \
 \ : ord_iso((A+B)*C, rmult(A+B, radd(A,r,B,s), C, t), \
 \           (A*C)+(B*C), radd(A*C, rmult(A,r,C,t), B*C, rmult(B,s,C,t)))";
 by (resolve_tac [sum_prod_distrib_bij RS ord_isoI] 1);
diff -r 56544d061e1d -r e0baea4d485a src/ZF/OrderType.ML
--- a/src/ZF/OrderType.ML	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/OrderType.ML	Fri Oct 10 18:23:31 1997 +0200
@@ -310,7 +310,7 @@
 
 (** Addition with 0 **)
 
-goal OrderType.thy "(lam z:A+0. case(%x.x, %y.y, z)) : bij(A+0, A)";
+goal OrderType.thy "(lam z:A+0. case(%x. x, %y. y, z)) : bij(A+0, A)";
 by (res_inst_tac [("d", "Inl")] lam_bijective 1);
 by (safe_tac (!claset));
 by (ALLGOALS Asm_simp_tac);
@@ -323,7 +323,7 @@
 by (fast_tac (!claset addss (!simpset addsimps [radd_Inl_iff, Memrel_iff])) 1);
 qed "ordertype_sum_0_eq";
 
-goal OrderType.thy "(lam z:0+A. case(%x.x, %y.y, z)) : bij(0+A, A)";
+goal OrderType.thy "(lam z:0+A. case(%x. x, %y. y, z)) : bij(0+A, A)";
 by (res_inst_tac [("d", "Inr")] lam_bijective 1);
 by (safe_tac (!claset));
 by (ALLGOALS Asm_simp_tac);
@@ -343,7 +343,7 @@
  "!!A B. a:A ==>  \
 \        (lam x:pred(A,a,r). Inl(x))    \
 \        : bij(pred(A,a,r), pred(A+B, Inl(a), radd(A,r,B,s)))";
-by (res_inst_tac [("d", "case(%x.x, %y.y)")] lam_bijective 1);
+by (res_inst_tac [("d", "case(%x. x, %y. y)")] lam_bijective 1);
 by (safe_tac (!claset));
 by (ALLGOALS
     (asm_full_simp_tac 
@@ -363,7 +363,7 @@
  "!!A B. b:B ==>  \
 \        id(A+pred(B,b,s))      \
 \        : bij(A+pred(B,b,s), pred(A+B, Inr(b), radd(A,r,B,s)))";
-by (res_inst_tac [("d", "%z.z")] lam_bijective 1);
+by (res_inst_tac [("d", "%z. z")] lam_bijective 1);
 by (safe_tac (!claset));
 by (ALLGOALS (Asm_full_simp_tac));
 qed "pred_Inr_bij";
@@ -592,7 +592,7 @@
 
 goal OrderType.thy
     "!!A B. A<=B ==> (lam y:B. if(y:A, Inl(y), Inr(y))) : bij(B, A+(B-A))";
-by (res_inst_tac [("d", "case(%x.x, %y.y)")] lam_bijective 1);
+by (res_inst_tac [("d", "case(%x. x, %y. y)")] lam_bijective 1);
 by (blast_tac (!claset addSIs [if_type]) 1);
 by (fast_tac (!claset addSIs [case_type]) 1);
 by (etac sumE 2);
diff -r 56544d061e1d -r e0baea4d485a src/ZF/Perm.ML
--- a/src/ZF/Perm.ML	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Perm.ML	Fri Oct 10 18:23:31 1997 +0200
@@ -37,7 +37,7 @@
     "[| !!x. x:A ==> c(x): B;           \
 \       !!y. y:B ==> d(y): A;           \
 \       !!y. y:B ==> c(d(y)) = y        \
-\    |] ==> (lam x:A.c(x)) : surj(A,B)";
+\    |] ==> (lam x:A. c(x)) : surj(A,B)";
 by (res_inst_tac [("d", "d")] f_imp_surjective 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps ([lam_type]@prems)) ));
 qed "lam_surjective";
@@ -77,7 +77,7 @@
 val prems = goal Perm.thy
     "[| !!x. x:A ==> c(x): B;           \
 \       !!x. x:A ==> d(c(x)) = x        \
-\    |] ==> (lam x:A.c(x)) : inj(A,B)";
+\    |] ==> (lam x:A. c(x)) : inj(A,B)";
 by (res_inst_tac [("d", "d")] f_imp_injective 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps ([lam_type]@prems)) ));
 qed "lam_injective";
@@ -100,7 +100,7 @@
 \       !!y. y:B ==> d(y): A;           \
 \       !!x. x:A ==> d(c(x)) = x;       \
 \       !!y. y:B ==> c(d(y)) = y        \
-\    |] ==> (lam x:A.c(x)) : bij(A,B)";
+\    |] ==> (lam x:A. c(x)) : bij(A,B)";
 by (REPEAT (ares_tac (prems @ [IntI, lam_injective, lam_surjective]) 1));
 qed "lam_bijective";
 
@@ -329,7 +329,7 @@
 (*Simplifies compositions of lambda-abstractions*)
 val [prem] = goal Perm.thy
     "[| !!x. x:A ==> b(x): B    \
-\    |] ==> (lam y:B.c(y)) O (lam x:A. b(x)) = (lam x:A. c(b(x)))";
+\    |] ==> (lam y:B. c(y)) O (lam x:A. b(x)) = (lam x:A. c(b(x)))";
 by (rtac fun_extension 1);
 by (rtac comp_fun 1);
 by (rtac lam_funtype 2);
@@ -427,7 +427,7 @@
     "!!f A B. [| f: A->B;  g: B->A |] ==> \
 \             f O g = id(B) <-> (ALL y:B. f`(g`y)=y)";
 by (safe_tac (!claset));
-by (dres_inst_tac [("t", "%h.h`y ")] subst_context 1);
+by (dres_inst_tac [("t", "%h. h`y ")] subst_context 1);
 by (Asm_full_simp_tac 1);
 by (rtac fun_extension 1);
 by (REPEAT (ares_tac [comp_fun, lam_type] 1));
diff -r 56544d061e1d -r e0baea4d485a src/ZF/QPair.ML
--- a/src/ZF/QPair.ML	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/QPair.ML	Fri Oct 10 18:23:31 1997 +0200
@@ -125,7 +125,7 @@
 
 (*A META-equality, so that it applies to higher types as well...*)
 qed_goalw "qsplit" thy [qsplit_def]
-    "qsplit(%x y.c(x,y), <a;b>) == c(a,b)"
+    "qsplit(%x y. c(x,y), <a;b>) == c(a,b)"
  (fn _ => [ (Simp_tac 1),
             (rtac reflexive_thm 1) ]);
 
@@ -134,7 +134,7 @@
 qed_goal "qsplit_type" thy
     "[|  p:QSigma(A,B);   \
 \        !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x;y>) \
-\    |] ==> qsplit(%x y.c(x,y), p) : C(p)"
+\    |] ==> qsplit(%x y. c(x,y), p) : C(p)"
  (fn major::prems=>
   [ (rtac (major RS QSigmaE) 1),
     (asm_simp_tac (!simpset addsimps prems) 1) ]);
@@ -322,7 +322,7 @@
 by (Blast_tac 1);
 qed "Part_QInr";
 
-goal thy "Part(A <+> B, %x.QInr(h(x))) = {QInr(y). y: Part(B,h)}";
+goal thy "Part(A <+> B, %x. QInr(h(x))) = {QInr(y). y: Part(B,h)}";
 by (Blast_tac 1);
 qed "Part_QInr2";
 
diff -r 56544d061e1d -r e0baea4d485a src/ZF/Resid/Confluence.ML
--- a/src/ZF/Resid/Confluence.ML	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Resid/Confluence.ML	Fri Oct 10 18:23:31 1997 +0200
@@ -21,7 +21,7 @@
 
 
 goalw Confluence.thy [confluence_def,strip_def] 
-    "!!u.strip==> confluence(Spar_red)";
+    "!!u. strip==> confluence(Spar_red)";
 by (resolve_tac [impI RS allI RS allI] 1);
 by (etac Spar_red.induct 1);
 by (Fast_tac  1);
diff -r 56544d061e1d -r e0baea4d485a src/ZF/Resid/Conversion.ML
--- a/src/ZF/Resid/Conversion.ML	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Resid/Conversion.ML	Fri Oct 10 18:23:31 1997 +0200
@@ -10,7 +10,7 @@
 AddIs (Sconv.intrs @ Sconv1.intrs);
 
 goal Conversion.thy  
-    "!!u.m<--->n ==> n<--->m";
+    "!!u. m<--->n ==> n<--->m";
 by (etac Sconv.induct 1);
 by (etac Sconv1.induct 1);
 by (ALLGOALS Blast_tac);
@@ -21,7 +21,7 @@
 (* ------------------------------------------------------------------------- *)
 
 goal Conversion.thy  
-    "!!u.m<--->n ==> EX p.(m --->p) & (n ---> p)";
+    "!!u. m<--->n ==> EX p.(m --->p) & (n ---> p)";
 by (etac Sconv.induct 1);
 by (etac Sconv1.induct 1);
 by (blast_tac (!claset addIs [red1D1,redD2]) 1);
diff -r 56544d061e1d -r e0baea4d485a src/ZF/Resid/Cube.ML
--- a/src/ZF/Resid/Cube.ML	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Resid/Cube.ML	Fri Oct 10 18:23:31 1997 +0200
@@ -18,8 +18,8 @@
 
 (* Having more assumptions than needed -- removed below  *)
 goal Cube.thy 
-    "!!u.v<==u ==> \
-\   regular(u)-->(ALL w.w~v-->w~u-->  \
+    "!!u. v<==u ==> \
+\   regular(u)-->(ALL w. w~v-->w~u-->  \
 \             w |> u = (w|>v) |> (u|>v))";
 by (etac Ssub.induct 1);
 by (ALLGOALS (asm_simp_tac prism_ss));
diff -r 56544d061e1d -r e0baea4d485a src/ZF/Resid/Redex.thy
--- a/src/ZF/Resid/Redex.thy	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Resid/Redex.thy	Fri Oct 10 18:23:31 1997 +0200
@@ -22,7 +22,7 @@
 defs
   redex_rec_def
    "redex_rec(p,b,c,d) == 
-   Vrec(p, %p g.redexes_case(b, %x.c(x,g`x),   
-                             %n x y.d(n, x, y, g`x, g`y), p))"
+   Vrec(p, %p g. redexes_case(b, %x. c(x,g`x),   
+                             %n x y. d(n, x, y, g`x, g`y), p))"
 end
 
diff -r 56544d061e1d -r e0baea4d485a src/ZF/Resid/Reduction.ML
--- a/src/ZF/Resid/Reduction.ML	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Resid/Reduction.ML	Fri Oct 10 18:23:31 1997 +0200
@@ -76,23 +76,23 @@
 (* ------------------------------------------------------------------------- *)
 
 
-goal Reduction.thy "!!u.m:lambda==> m =1=> m";
+goal Reduction.thy "!!u. m:lambda==> m =1=> m";
 by (eresolve_tac [lambda.induct] 1);
 by (ALLGOALS (Asm_simp_tac ));
 qed "refl_par_red1";
 
-goal Reduction.thy "!!u.m-1->n ==> m=1=>n";
+goal Reduction.thy "!!u. m-1->n ==> m=1=>n";
 by (etac Sred1.induct 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [refl_par_red1]) ));
 qed "red1_par_red1";
 
-goal Reduction.thy "!!u.m--->n ==> m===>n";
+goal Reduction.thy "!!u. m--->n ==> m===>n";
 by (etac Sred.induct 1);
 by (resolve_tac [Spar_red.trans] 3);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [refl_par_red1,red1_par_red1]) ));
 qed "red_par_red";
 
-goal Reduction.thy "!!u.m===>n ==> m--->n";
+goal Reduction.thy "!!u. m===>n ==> m--->n";
 by (etac Spar_red.induct 1);
 by (etac Spar_red1.induct 1);
 by (resolve_tac [Sred.trans] 5);
@@ -105,7 +105,7 @@
 (* ------------------------------------------------------------------------- *)
 
 goal Reduction.thy  
-    "!!u.m=1=>n ==> EX v. m|>v = n & m~v & regular(v)";
+    "!!u. m=1=>n ==> EX v. m|>v = n & m~v & regular(v)";
 by (etac Spar_red1.induct 1);
 by Safe_tac;
 by (ALLGOALS (REPEAT o (resolve_tac [exI,conjI])));
@@ -119,14 +119,14 @@
 (* ------------------------------------------------------------------------- *)
 
 goal Reduction.thy  
-    "!!u.u:redexes ==> \
+    "!!u. u:redexes ==> \
 \           ALL k:nat. unmark(lift_rec(u,k)) = lift_rec(unmark(u),k)";
 by (eresolve_tac [redexes.induct] 1);
 by (ALLGOALS (asm_full_simp_tac (addsplit (!simpset))));
 qed "unmmark_lift_rec";
 
 goal Reduction.thy  
-    "!!u.v:redexes ==> ALL k:nat.ALL u:redexes.  \
+    "!!u. v:redexes ==> ALL k:nat. ALL u:redexes.  \
 \         unmark(subst_rec(u,v,k)) = subst_rec(unmark(u),unmark(v),k)";
 by (eresolve_tac [redexes.induct] 1);
 by (ALLGOALS (asm_full_simp_tac 
@@ -139,7 +139,7 @@
 (* ------------------------------------------------------------------------- *)
 
 goal Reduction.thy  
-    "!!u.u~v ==> regular(v) --> unmark(u) =1=> unmark(u|>v)";
+    "!!u. u~v ==> regular(v) --> unmark(u) =1=> unmark(u|>v)";
 by (etac Scomp.induct 1);
 by (ALLGOALS (asm_full_simp_tac (reducL_ss addsimps [unmmark_subst_rec]) ));
 by (dres_inst_tac [("psi", "Fun(?u) =1=> ?w")] asm_rl 1);
diff -r 56544d061e1d -r e0baea4d485a src/ZF/Resid/Residuals.ML
--- a/src/ZF/Resid/Residuals.ML	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Resid/Residuals.ML	Fri Oct 10 18:23:31 1997 +0200
@@ -44,13 +44,13 @@
 (* ------------------------------------------------------------------------- *)
 
 goal Residuals.thy 
-    "!!u.residuals(u,v,w) ==> ALL w1.residuals(u,v,w1) --> w1 = w";
+    "!!u. residuals(u,v,w) ==> ALL w1. residuals(u,v,w1) --> w1 = w";
 by (etac Sres.induct 1);
 by (ALLGOALS Fast_tac);
 qed_spec_mp "residuals_function";
 
 goal Residuals.thy 
-    "!!u.u~v ==> regular(v) --> (EX w.residuals(u,v,w))";
+    "!!u. u~v ==> regular(v) --> (EX w. residuals(u,v,w))";
 by (etac Scomp.induct 1);
 by (ALLGOALS Fast_tac);
 qed "residuals_intro";
@@ -74,7 +74,7 @@
                           addSEs [comp_resfuncE]);
 
 goalw Residuals.thy [res_func_def]
-    "!!n.n:nat ==> Var(n) |> Var(n) = Var(n)";
+    "!!n. n:nat ==> Var(n) |> Var(n) = Var(n)";
 by (fast_tac resfunc_cs 1);
 qed "res_Var";
 
@@ -119,13 +119,13 @@
 (* ------------------------------------------------------------------------- *)
 
 goal Residuals.thy 
-    "!!u.u<==v ==> u~v";
+    "!!u. u<==v ==> u~v";
 by (etac Ssub.induct 1);
 by (ALLGOALS Asm_simp_tac);
 qed "sub_comp";
 
 goal Residuals.thy 
-    "!!u.u<==v  ==> regular(v) --> regular(u)";
+    "!!u. u<==v  ==> regular(v) --> regular(u)";
 by (etac Ssub.induct 1);
 by (ALLGOALS (asm_simp_tac res1L_ss));
 qed "sub_preserve_reg";
@@ -136,13 +136,13 @@
 by (etac Scomp.induct 1);
 by Safe_tac;
 by (ALLGOALS (asm_full_simp_tac ((addsplit (!simpset)) addsimps [lift_subst])));
-by (dres_inst_tac [("psi", "ALL x:nat.Fun(?u(x)) |> ?v(x) = ?w(x)")] asm_rl 1);
+by (dres_inst_tac [("psi", "ALL x:nat. Fun(?u(x)) |> ?v(x) = ?w(x)")] asm_rl 1);
 by (Asm_full_simp_tac 1);
 qed "residuals_lift_rec";
 
 goal Residuals.thy 
-    "!!u.u1~u2 ==>  ALL v1 v2.v1~v2 --> regular(v2) --> regular(u2) -->\
-\   (ALL n:nat.subst_rec(v1,u1,n) |> subst_rec(v2,u2,n) = \
+    "!!u. u1~u2 ==>  ALL v1 v2. v1~v2 --> regular(v2) --> regular(u2) -->\
+\   (ALL n:nat. subst_rec(v1,u1,n) |> subst_rec(v2,u2,n) = \
 \              subst_rec(v1 |> v2, u1 |> u2,n))";
 by (etac Scomp.induct 1);
 by Safe_tac;
@@ -164,7 +164,7 @@
 (* ------------------------------------------------------------------------- *)
 
 goal Residuals.thy 
-    "!!u.u~v ==> ALL w. u~w --> v~w --> regular(w) --> (u|>w) ~ (v|>w)";
+    "!!u. u~v ==> ALL w. u~w --> v~w --> regular(w) --> (u|>w) ~ (v|>w)";
 by (etac Scomp.induct 1);
 by (ALLGOALS (asm_simp_tac res1L_ss));
 by (dresolve_tac [spec RS mp RS mp RS mp] 1 
@@ -176,7 +176,7 @@
 
 
 goal Residuals.thy 
-    "!!u.u~v ==> regular(u) --> regular(v) --> regular(u|>v)";
+    "!!u. u~v ==> regular(u) --> regular(v) --> regular(u|>v)";
 by (etac Scomp.induct 1);
 by (safe_tac (!claset));
 by (TRYALL (dres_inst_tac [("psi", "regular(Fun(?u) |> ?v)")] asm_rl));
@@ -188,13 +188,13 @@
 (* ------------------------------------------------------------------------- *)
 
 goal Residuals.thy 
-    "!!u.u~v ==> v ~ (u un v)";
+    "!!u. u~v ==> v ~ (u un v)";
 by (etac Scomp.induct 1);
 by (ALLGOALS Asm_full_simp_tac);
 qed "union_preserve_comp";
 
 goal Residuals.thy 
-    "!!u.u ~ v ==> regular(v) --> u|>v = (u un v)|>v";
+    "!!u. u ~ v ==> regular(v) --> u|>v = (u un v)|>v";
 by (etac Scomp.induct 1);
 by (safe_tac (!claset));
 by (dres_inst_tac [("psi", "Fun(?u) |> ?v = ?w")] asm_rl 3);
diff -r 56544d061e1d -r e0baea4d485a src/ZF/Resid/Residuals.thy
--- a/src/ZF/Resid/Residuals.thy	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Resid/Residuals.thy	Fri Oct 10 18:23:31 1997 +0200
@@ -31,6 +31,6 @@
   type_intrs    "[subst_type]@nat_typechecks@redexes.intrs@bool_typechecks"
 
 rules
-  res_func_def  "u |> v == THE w.residuals(u,v,w)"
+  res_func_def  "u |> v == THE w. residuals(u,v,w)"
 end
 
diff -r 56544d061e1d -r e0baea4d485a src/ZF/Resid/SubUnion.ML
--- a/src/ZF/Resid/SubUnion.ML	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Resid/SubUnion.ML	Fri Oct 10 18:23:31 1997 +0200
@@ -22,7 +22,7 @@
 (* ------------------------------------------------------------------------- *)
 
 goalw SubUnion.thy [union_def]
-    "!!u.n:nat==>Var(n) un Var(n)=Var(n)";
+    "!!u. n:nat==>Var(n) un Var(n)=Var(n)";
 by (Asm_simp_tac 1);
 by (simp_tac (rank_ss addsimps redexes.con_defs)  1);
 qed "union_Var";
@@ -65,13 +65,13 @@
 (*    comp proofs                                                            *)
 (* ------------------------------------------------------------------------- *)
 
-goal SubUnion.thy "!!u.u:redexes ==> u ~ u";
+goal SubUnion.thy "!!u. u:redexes ==> u ~ u";
 by (eresolve_tac [redexes.induct] 1);
 by (ALLGOALS Fast_tac);
 qed "comp_refl";
 
 goal SubUnion.thy 
-    "!!u.u ~ v ==> v ~ u";
+    "!!u. u ~ v ==> v ~ u";
 by (etac Scomp.induct 1);
 by (ALLGOALS Fast_tac);
 qed "comp_sym";
@@ -83,7 +83,7 @@
 
 
 goal SubUnion.thy 
-    "!!u.u ~ v ==> ALL w.v ~ w-->u ~ w";
+    "!!u. u ~ v ==> ALL w. v ~ w-->u ~ w";
 by (etac Scomp.induct 1);
 by (ALLGOALS Fast_tac);
 qed_spec_mp "comp_trans";
@@ -93,21 +93,21 @@
 (* ------------------------------------------------------------------------- *)
 
 goal SubUnion.thy 
-    "!!u.u ~ v ==> u <== (u un v)";
+    "!!u. u ~ v ==> u <== (u un v)";
 by (etac Scomp.induct 1);
 by (etac boolE 3);
 by (ALLGOALS Asm_full_simp_tac);
 qed "union_l";
 
 goal SubUnion.thy 
-    "!!u.u ~ v ==> v <== (u un v)";
+    "!!u. u ~ v ==> v <== (u un v)";
 by (etac Scomp.induct 1);
 by (eres_inst_tac [("c","b2")] boolE 3);
 by (ALLGOALS Asm_full_simp_tac);
 qed "union_r";
 
 goal SubUnion.thy 
-    "!!u.u ~ v ==> u un v = v un u";
+    "!!u. u ~ v ==> u un v = v un u";
 by (etac Scomp.induct 1);
 by (ALLGOALS(asm_simp_tac (!simpset addsimps [or_commute])));
 qed "union_sym";
@@ -117,7 +117,7 @@
 (* ------------------------------------------------------------------------- *)
 
 goal SubUnion.thy 
-    "!!u.u ~ v ==> regular(u)-->regular(v)-->regular(u un v)";
+    "!!u. u ~ v ==> regular(u)-->regular(v)-->regular(u un v)";
 by (etac Scomp.induct 1);
 by (ALLGOALS(asm_full_simp_tac
              (!simpset setloop(SELECT_GOAL (safe_tac (!claset))))));
diff -r 56544d061e1d -r e0baea4d485a src/ZF/Resid/SubUnion.thy
--- a/src/ZF/Resid/SubUnion.thy	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Resid/SubUnion.thy	Fri Oct 10 18:23:31 1997 +0200
@@ -51,9 +51,8 @@
 
 defs
   union_def  "u un v == redex_rec(u,   
-         %i.lam t:redexes.redexes_case(%j.Var(i), %x.0, %b x y.0, t),   
-      %x m.lam t:redexes.redexes_case(%j.0, %y.Fun(m`y), %b y z.0, t),   
-%b x y m p.lam t:redexes.redexes_case(%j.0, %y.0,   
+         %i. lam t:redexes. redexes_case(%j. Var(i), %x.0, %b x y.0, t),   
+      %x m. lam t:redexes. redexes_case(%j.0, %y. Fun(m`y), %b y z.0, t),   
+%b x y m p. lam t:redexes. redexes_case(%j.0, %y.0,   
                                        %c z u. App(b or c, m`z, p`u), t))`v"
 end
-
diff -r 56544d061e1d -r e0baea4d485a src/ZF/Resid/Substitution.ML
--- a/src/ZF/Resid/Substitution.ML	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Resid/Substitution.ML	Fri Oct 10 18:23:31 1997 +0200
@@ -113,7 +113,7 @@
 
 
 goal Substitution.thy  
-    "!!n.u:redexes ==> ALL k:nat.lift_rec(u,k):redexes";
+    "!!n. u:redexes ==> ALL k:nat. lift_rec(u,k):redexes";
 by (eresolve_tac [redexes.induct] 1);
 by (ALLGOALS(asm_full_simp_tac 
     ((addsplit (!simpset)) addsimps [lift_rec_Fun,lift_rec_App])));
@@ -121,7 +121,7 @@
 val lift_rec_type = lift_rec_type_a RS bspec;
 
 goalw Substitution.thy [] 
-    "!!n.v:redexes ==>  ALL n:nat.ALL u:redexes.subst_rec(u,v,n):redexes";
+    "!!n. v:redexes ==>  ALL n:nat. ALL u:redexes. subst_rec(u,v,n):redexes";
 by (eresolve_tac [redexes.induct] 1);
 by (ALLGOALS(asm_full_simp_tac 
     ((addsplit (!simpset)) addsimps [subst_Fun,subst_App,
@@ -140,7 +140,7 @@
 (* ------------------------------------------------------------------------- *)
 
 goalw Substitution.thy [] 
-    "!!n.u:redexes ==> ALL n:nat.ALL i:nat.i le n -->   \
+    "!!n. u:redexes ==> ALL n:nat. ALL i:nat. i le n -->   \
 \       (lift_rec(lift_rec(u,i),succ(n)) = lift_rec(lift_rec(u,n),i))";
 by ((eresolve_tac [redexes.induct] 1)
     THEN (ALLGOALS Asm_simp_tac));
@@ -159,8 +159,8 @@
 qed "lift_lift";
 
 goal Substitution.thy 
-    "!!n.v:redexes ==>  \
-\      ALL n:nat.ALL m:nat.ALL u:redexes.n le m-->\
+    "!!n. v:redexes ==>  \
+\      ALL n:nat. ALL m:nat. ALL u:redexes. n le m-->\
 \         lift_rec(subst_rec(u,v,n),m) = \
 \              subst_rec(lift_rec(u,m),lift_rec(v,succ(m)),n)";
 by ((eresolve_tac [redexes.induct] 1)
@@ -186,8 +186,8 @@
 
 
 goalw Substitution.thy [] 
-    "!!n.v:redexes ==>  \
-\      ALL n:nat.ALL m:nat.ALL u:redexes.m le n-->\
+    "!!n. v:redexes ==>  \
+\      ALL n:nat. ALL m:nat. ALL u:redexes. m le n-->\
 \         lift_rec(subst_rec(u,v,n),m) = \
 \              subst_rec(lift_rec(u,m),lift_rec(v,m),succ(n))";
 by ((eresolve_tac [redexes.induct] 1)
@@ -208,8 +208,8 @@
 
 
 goalw Substitution.thy [] 
-    "!!n.u:redexes ==>  \
-\       ALL n:nat.ALL v:redexes.subst_rec(v,lift_rec(u,n),n) =  u";
+    "!!n. u:redexes ==>  \
+\       ALL n:nat. ALL v:redexes. subst_rec(v,lift_rec(u,n),n) =  u";
 by ((eresolve_tac [redexes.induct] 1)
     THEN (ALLGOALS Asm_simp_tac));
 by Safe_tac;
@@ -220,8 +220,8 @@
 qed "subst_rec_lift_rec";
 
 goal Substitution.thy  
-    "!!n.v:redexes ==>  \
-\       ALL m:nat.ALL n:nat.ALL u:redexes.ALL w:redexes.m le  n --> \
+    "!!n. v:redexes ==>  \
+\       ALL m:nat. ALL n:nat. ALL u:redexes. ALL w:redexes. m le  n --> \
 \    subst_rec(subst_rec(w,u,n),subst_rec(lift_rec(w,m),v,succ(n)),m)=\
 \    subst_rec(w,subst_rec(u,v,m),n)";
 by ((eresolve_tac [redexes.induct] 1) THEN 
@@ -263,13 +263,13 @@
 
 
 goal Substitution.thy
-    "!!n.[|n:nat; u ~ v|]==> ALL m:nat.lift_rec(u,m) ~ lift_rec(v,m)";
+    "!!n.[|n:nat; u ~ v|]==> ALL m:nat. lift_rec(u,m) ~ lift_rec(v,m)";
 by (etac Scomp.induct 1);
 by (ALLGOALS(asm_simp_tac (!simpset addsimps [comp_refl])));
 qed "lift_rec_preserve_comp";
 
 goal Substitution.thy
-    "!!n.u2 ~ v2 ==> ALL m:nat.ALL u1:redexes.ALL v1:redexes.\
+    "!!n. u2 ~ v2 ==> ALL m:nat. ALL u1:redexes. ALL v1:redexes.\
 \            u1 ~ v1--> subst_rec(u1,u2,m) ~ subst_rec(v1,v2,m)";
 by (etac Scomp.induct 1);
 by (ALLGOALS(asm_full_simp_tac ((addsplit (!simpset)) addsimps 
@@ -277,14 +277,14 @@
 qed "subst_rec_preserve_comp";
 
 goal Substitution.thy
-    "!!n.regular(u) ==> ALL m:nat.regular(lift_rec(u,m))";
+    "!!n. regular(u) ==> ALL m:nat. regular(lift_rec(u,m))";
 by (eresolve_tac [Sreg.induct] 1);
 by (ALLGOALS(asm_full_simp_tac (addsplit (!simpset))));
 qed "lift_rec_preserve_reg";
 
 goal Substitution.thy
-    "!!n.regular(v) ==>  \
-\       ALL m:nat.ALL u:redexes.regular(u)-->regular(subst_rec(u,v,m))";
+    "!!n. regular(v) ==>  \
+\       ALL m:nat. ALL u:redexes. regular(u)-->regular(subst_rec(u,v,m))";
 by (eresolve_tac [Sreg.induct] 1);
 by (ALLGOALS(asm_full_simp_tac ((addsplit (!simpset)) addsimps 
             [lift_rec_preserve_reg])));
diff -r 56544d061e1d -r e0baea4d485a src/ZF/Resid/Substitution.thy
--- a/src/ZF/Resid/Substitution.thy	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Resid/Substitution.thy	Fri Oct 10 18:23:31 1997 +0200
@@ -18,9 +18,9 @@
   
 defs
   lift_rec_def  "lift_rec(r,kg) ==   
-                     redex_rec(r,%i.(lam k:nat.if(i<k,Var(i),Var(succ(i)))), 
-                                 %x m.(lam k:nat.Fun(m`(succ(k)))),   
-                                 %b x y m p.lam k:nat.App(b,m`k,p`k))`kg"
+                     redex_rec(r,%i.(lam k:nat. if(i<k,Var(i),Var(succ(i)))), 
+                                 %x m.(lam k:nat. Fun(m`(succ(k)))),   
+                                 %b x y m p. lam k:nat. App(b,m`k,p`k))`kg"
 
   
 (* subst_rec(u,Var(i),k)     = if k<i then Var(i-1)
@@ -32,12 +32,12 @@
 *)
   subst_rec_def "subst_rec(u,t,kg) ==   
                      redex_rec(t,   
-                       %i.(lam r:redexes.lam k:nat.   
+                       %i.(lam r:redexes. lam k:nat.   
                               if(k<i,Var(i#-1),   
                                 if(k=i,r,Var(i)))),   
-                       %x m.(lam r:redexes.lam k:nat.   
+                       %x m.(lam r:redexes. lam k:nat.   
                              Fun(m`(lift(r))`(succ(k)))),   
-                       %b x y m p.lam r:redexes.lam k:nat.   
+                       %b x y m p. lam r:redexes. lam k:nat.   
                               App(b,m`r`k,p`r`k))`u`kg"
 
 
diff -r 56544d061e1d -r e0baea4d485a src/ZF/Resid/Terms.ML
--- a/src/ZF/Resid/Terms.ML	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Resid/Terms.ML	Fri Oct 10 18:23:31 1997 +0200
@@ -42,13 +42,13 @@
 (* ------------------------------------------------------------------------- *)
 
 goalw Terms.thy [unmark_def] 
-    "!!u.u:redexes ==> unmark(u):lambda";
+    "!!u. u:redexes ==> unmark(u):lambda";
 by (eresolve_tac [redexes.induct] 1);
 by (ALLGOALS Asm_simp_tac);
 qed "unmark_type";
 
 goal Terms.thy  
-    "!!u.u:lambda ==> unmark(u) = u";
+    "!!u. u:lambda ==> unmark(u) = u";
 by (eresolve_tac [lambda.induct] 1);
 by (ALLGOALS Asm_simp_tac);
 qed "lambda_unmark";
@@ -59,14 +59,14 @@
 (* ------------------------------------------------------------------------- *)
 
 goal Terms.thy  
-    "!!u.[|v:lambda|]==> ALL k:nat.lift_rec(v,k):lambda";
+    "!!u.[|v:lambda|]==> ALL k:nat. lift_rec(v,k):lambda";
 by (eresolve_tac [lambda.induct] 1);
 by (ALLGOALS(asm_full_simp_tac (addsplit (!simpset))));
 qed "liftL_typea";
 val liftL_type =liftL_typea RS bspec ;
 
 goal Terms.thy  
-    "!!n.[|v:lambda|]==>  ALL n:nat.ALL u:lambda.subst_rec(u,v,n):lambda";
+    "!!n.[|v:lambda|]==>  ALL n:nat. ALL u:lambda. subst_rec(u,v,n):lambda";
 by (eresolve_tac [lambda.induct] 1);
 by (ALLGOALS(asm_full_simp_tac ((addsplit (!simpset)) addsimps [liftL_type])));
 qed "substL_typea";
diff -r 56544d061e1d -r e0baea4d485a src/ZF/Resid/Terms.thy
--- a/src/ZF/Resid/Terms.thy	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Resid/Terms.thy	Fri Oct 10 18:23:31 1997 +0200
@@ -24,9 +24,9 @@
   type_intrs    "redexes.intrs@bool_typechecks"
 
 defs
-  unmark_def    "unmark(u) == redex_rec(u,%i.Var(i),   
-                                          %x m.Fun(m),   
-                                          %b x y m p.Apl(m,p))"
+  unmark_def    "unmark(u) == redex_rec(u,%i. Var(i),   
+                                          %x m. Fun(m),   
+                                          %b x y m p. Apl(m,p))"
 end
 
 
diff -r 56544d061e1d -r e0baea4d485a src/ZF/Sum.ML
--- a/src/ZF/Sum.ML	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/Sum.ML	Fri Oct 10 18:23:31 1997 +0200
@@ -200,11 +200,11 @@
 by (etac CollectD1 1);
 qed "PartD1";
 
-goal Sum.thy "Part(A,%x.x) = A";
+goal Sum.thy "Part(A,%x. x) = A";
 by (Blast_tac 1);
 qed "Part_id";
 
-goal Sum.thy "Part(A+B, %x.Inr(h(x))) = {Inr(y). y: Part(B,h)}";
+goal Sum.thy "Part(A+B, %x. Inr(h(x))) = {Inr(y). y: Part(B,h)}";
 by (Blast_tac 1);
 qed "Part_Inr2";
 
diff -r 56544d061e1d -r e0baea4d485a src/ZF/WF.thy
--- a/src/ZF/WF.thy	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/WF.thy	Fri Oct 10 18:23:31 1997 +0200
@@ -26,7 +26,7 @@
   is_recfun_def  "is_recfun(r,a,H,f) == 
                         (f = (lam x: r-``{a}. H(x, restrict(f, r-``{x}))))"
 
-  the_recfun_def "the_recfun(r,a,H) == (THE f.is_recfun(r,a,H,f))"
+  the_recfun_def "the_recfun(r,a,H) == (THE f. is_recfun(r,a,H,f))"
 
   wftrec_def     "wftrec(r,a,H) == H(a, the_recfun(r,a,H))"
 
diff -r 56544d061e1d -r e0baea4d485a src/ZF/ZF.ML
--- a/src/ZF/ZF.ML	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/ZF.ML	Fri Oct 10 18:23:31 1997 +0200
@@ -53,7 +53,7 @@
 val ball_tac = dtac bspec THEN' assume_tac;
 
 (*Trival rewrite rule;   (ALL x:A.P)<->P holds only if A is nonempty!*)
-qed_goal "ball_triv" ZF.thy "(ALL x:A.P) <-> ((EX x. x:A) --> P)"
+qed_goal "ball_triv" ZF.thy "(ALL x:A. P) <-> ((EX x. x:A) --> P)"
  (fn _=> [ simp_tac (!simpset addsimps [Ball_def]) 1 ]);
 Addsimps [ball_triv];
 
@@ -70,7 +70,7 @@
 
 (*Not of the general form for such rules; ~EX has become ALL~ *)
 qed_goal "bexCI" ZF.thy 
-   "[| ALL x:A. ~P(x) ==> P(a);  a: A |] ==> EX x:A.P(x)"
+   "[| ALL x:A. ~P(x) ==> P(a);  a: A |] ==> EX x:A. P(x)"
  (fn prems=>
   [ (rtac classical 1),
     (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1)) ]);
@@ -86,7 +86,7 @@
 AddSEs [bexE];
 
 (*We do not even have (EX x:A. True) <-> True unless A is nonempty!!*)
-qed_goal  "bex_triv" ZF.thy "(EX x:A.P) <-> ((EX x. x:A) & P)"
+qed_goal  "bex_triv" ZF.thy "(EX x:A. P) <-> ((EX x. x:A) & P)"
  (fn _=> [ simp_tac (!simpset addsimps [Bex_def]) 1 ]);
 Addsimps [bex_triv];
 
@@ -101,7 +101,7 @@
 (*** Rules for subsets ***)
 
 qed_goalw "subsetI" ZF.thy [subset_def]
-    "(!!x.x:A ==> x:B) ==> A <= B"
+    "(!!x. x:A ==> x:B) ==> A <= B"
  (fn prems=> [ (REPEAT (ares_tac (prems @ [ballI]) 1)) ]);
 
 (*Rule in Modus Ponens style [was called subsetE] *)
@@ -271,7 +271,7 @@
     "b : {f(x). x:A} <-> (EX x:A. b=f(x))"
  (fn _ => [Blast_tac 1]);
 
-goal ZF.thy "{x.x:A} = A";
+goal ZF.thy "{x. x:A} = A";
 by (Blast_tac 1);
 qed "triv_RepFun";
 
@@ -344,7 +344,7 @@
     (REPEAT (eresolve_tac (prems@[asm_rl, RepFunE, subst]) 1)) ]);
 
 qed_goal "UN_cong" ZF.thy
-    "[| A=B;  !!x. x:B ==> C(x)=D(x) |] ==> (UN x:A.C(x)) = (UN x:B.D(x))"
+    "[| A=B;  !!x. x:B ==> C(x)=D(x) |] ==> (UN x:A. C(x)) = (UN x:B. D(x))"
  (fn prems=> [ (simp_tac (!simpset addsimps prems) 1) ]);
 
 (*No "Addcongs [UN_cong]" because UN is a combination of constants*)
@@ -404,7 +404,7 @@
     (rtac (minor RS RepFunI) 1) ]);
 
 qed_goal "INT_cong" ZF.thy
-    "[| A=B;  !!x. x:B ==> C(x)=D(x) |] ==> (INT x:A.C(x)) = (INT x:B.D(x))"
+    "[| A=B;  !!x. x:B ==> C(x)=D(x) |] ==> (INT x:A. C(x)) = (INT x:B. D(x))"
  (fn prems=> [ (simp_tac (!simpset addsimps prems) 1) ]);
 
 (*No "Addcongs [INT_cong]" because INT is a combination of constants*)
diff -r 56544d061e1d -r e0baea4d485a src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/ZF.thy	Fri Oct 10 18:23:31 1997 +0200
@@ -129,7 +129,7 @@
   "<x, y, z>"   == "<x, <y, z>>"
   "<x, y>"      == "Pair(x, y)"
   "%<x,y,zs>.b" == "split(%x <y,zs>.b)"
-  "%<x,y>.b"    == "split(%x y.b)"
+  "%<x,y>.b"    == "split(%x y. b)"
 
 
 syntax (symbols)
@@ -190,7 +190,7 @@
      The resulting set (for functional P) is the same as with
      PrimReplace, but the rules are simpler. *)
 
-  Replace_def   "Replace(A,P) == PrimReplace(A, %x y. (EX!z.P(x,z)) & P(x,y))"
+  Replace_def   "Replace(A,P) == PrimReplace(A, %x y. (EX!z. P(x,z)) & P(x,y))"
 
   (* Functional form of replacement -- analgous to ML's map functional *)
 
@@ -246,7 +246,7 @@
   Pi_def        "Pi(A,B)  == {f: Pow(Sigma(A,B)). A<=domain(f) & function(f)}"
 
   (* Restrict the function f to the domain A *)
-  restrict_def  "restrict(f,A) == lam x:A.f`x"
+  restrict_def  "restrict(f,A) == lam x:A. f`x"
 
 end
 
diff -r 56544d061e1d -r e0baea4d485a src/ZF/ex/BT.thy
--- a/src/ZF/ex/BT.thy	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/ex/BT.thy	Fri Oct 10 18:23:31 1997 +0200
@@ -20,7 +20,7 @@
   
 defs
   bt_rec_def
-    "bt_rec(t,c,h) == Vrec(t, %t g.bt_case(c, %x y z. h(x,y,z,g`y,g`z), t))"
+    "bt_rec(t,c,h) == Vrec(t, %t g. bt_case(c, %x y z. h(x,y,z,g`y,g`z), t))"
 
   n_nodes_def   "n_nodes(t) == bt_rec(t,  0,  %x y z r s. succ(r#+s))"
   n_leaves_def  "n_leaves(t) == bt_rec(t,  succ(0),  %x y z r s. r#+s)"
diff -r 56544d061e1d -r e0baea4d485a src/ZF/ex/Brouwer.ML
--- a/src/ZF/ex/Brouwer.ML	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/ex/Brouwer.ML	Fri Oct 10 18:23:31 1997 +0200
@@ -56,7 +56,7 @@
 
 (*In fact it's isomorphic to nat, but we need a recursion operator for
   Well to prove this.*)
-goal Brouwer.thy "Well(bool, %x.x) = 1 + (1 -> Well(bool, %x.x))";
+goal Brouwer.thy "Well(bool, %x. x) = 1 + (1 -> Well(bool, %x. x))";
 by (resolve_tac [Well_unfold RS trans] 1);
 by (simp_tac (!simpset addsimps [Sigma_bool, Pi_empty1, succ_def]) 1);
 qed "Well_bool_unfold";
diff -r 56544d061e1d -r e0baea4d485a src/ZF/ex/Limit.ML
--- a/src/ZF/ex/Limit.ML	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/ex/Limit.ML	Fri Oct 10 18:23:31 1997 +0200
@@ -150,7 +150,7 @@
 qed "isubI";
 
 val prems = goalw Limit.thy [isub_def]  (* isubE *)
-    "!!z.[|isub(D,X,x);[|x:set(D);  !!n.n:nat==>rel(D,X`n,x)|] ==> P|] ==> P";
+    "!!z.[|isub(D,X,x);[|x:set(D);  !!n. n:nat==>rel(D,X`n,x)|] ==> P|] ==> P";
 by (safe_tac (!claset));
 by (Asm_simp_tac 1);
 qed "isubE";
@@ -248,7 +248,7 @@
 (*----------------------------------------------------------------------*)
 
 val prems = goalw Limit.thy [pcpo_def]  (* pcpoI *)
-    "[|!!y.y:set(D)==>rel(D,x,y); x:set(D); cpo(D)|]==>pcpo(D)";
+    "[|!!y. y:set(D)==>rel(D,x,y); x:set(D); cpo(D)|]==>pcpo(D)";
 by (rtac conjI 1);
 by (resolve_tac prems 1);
 by (rtac bexI 1);
@@ -322,7 +322,7 @@
 qed "islub_const";
 
 val prems = goal Limit.thy  (* lub_const *)
-    "[|x:set(D); cpo(D)|] ==> lub(D,lam n:nat.x) = x";
+    "[|x:set(D); cpo(D)|] ==> lub(D,lam n:nat. x) = x";
 by (rtac islub_unique 1);
 by (rtac cpo_lub 1);
 by (rtac chain_const 1);
@@ -512,7 +512,7 @@
 qed "matrix_chain_right";
 
 val prems = goalw Limit.thy [matrix_def]  (* matrix_chainI *)
-    "[|!!x.x:nat==>chain(D,M`x);  !!y.y:nat==>chain(D,lam x:nat. M`x`y);   \
+    "[|!!x. x:nat==>chain(D,M`x);  !!y. y:nat==>chain(D,lam x:nat. M`x`y);   \
 \      M:nat->nat->set(D); cpo(D)|] ==> matrix(D,M)";
 by (safe_tac (!claset addSIs [ballI]));
 by (cut_inst_tac[("y1","m"),("n","n")](hd(tl prems) RS chain_rel) 2);
@@ -529,7 +529,7 @@
     (fn prems => [Asm_full_simp_tac 1]);
 
 val lemma2 = prove_goal Limit.thy
-    "!!z.[|x:nat; m:nat; rel(D,(lam n:nat.M`n`m1)`x,(lam n:nat.M`n`m1)`m)|] ==> \
+    "!!z.[|x:nat; m:nat; rel(D,(lam n:nat. M`n`m1)`x,(lam n:nat. M`n`m1)`m)|] ==> \
 \        rel(D,M`x`m1,M`m`m1)"
     (fn prems => [Asm_full_simp_tac 1]);
 
@@ -574,7 +574,7 @@
 qed "isub_lemma";
 
 val prems = goalw Limit.thy [chain_def]  (* matrix_chain_lub *)
-    "[|matrix(D,M); cpo(D)|] ==> chain(D,lam n:nat.lub(D,lam m:nat.M`n`m))";
+    "[|matrix(D,M); cpo(D)|] ==> chain(D,lam n:nat. lub(D,lam m:nat. M`n`m))";
 by (safe_tac (!claset));
 by (rtac lam_type 1);
 by (rtac islub_in 1);
@@ -1335,7 +1335,7 @@
 
 val prems = goalw Limit.thy [chain_def]  (* chain_iprod *)
     "[|chain(iprod(DD),X);  !!n. n:nat ==> cpo(DD`n); n:nat|] ==>  \
-\    chain(DD`n,lam m:nat.X`m`n)";
+\    chain(DD`n,lam m:nat. X`m`n)";
 by (safe_tac (!claset));
 by (rtac lam_type 1);
 by (rtac apply_type 1);
@@ -1350,7 +1350,7 @@
 
 val prems = goalw Limit.thy [islub_def,isub_def]  (* islub_iprod *)
     "[|chain(iprod(DD),X);  !!n. n:nat ==> cpo(DD`n)|] ==>   \
-\    islub(iprod(DD),X,lam n:nat. lub(DD`n,lam m:nat.X`m`n))";
+\    islub(iprod(DD),X,lam n:nat. lub(DD`n,lam m:nat. X`m`n))";
 by (safe_tac (!claset));
 by (rtac iprodI 1);
 by (rtac lam_type 1); 
@@ -1391,7 +1391,7 @@
 
 val prems = goalw Limit.thy [islub_def,isub_def]  (* lub_iprod *)
     "[|chain(iprod(DD),X);  !!n. n:nat ==> cpo(DD`n)|] ==>   \
-\    lub(iprod(DD),X) = (lam n:nat. lub(DD`n,lam m:nat.X`m`n))";
+\    lub(iprod(DD),X) = (lam n:nat. lub(DD`n,lam m:nat. X`m`n))";
 brr((cpo_lub RS islub_unique)::islub_iprod::cpo_iprod::prems) 1;
 qed "lub_iprod";
 
@@ -2758,7 +2758,7 @@
 qed "suffix_lemma";
 
 val mediatingI = prove_goalw Limit.thy [mediating_def]
-  "[|emb(E,G,t);  !!n.n:nat ==> f(n) = t O r(n) |]==>mediating(E,G,r,f,t)"
+  "[|emb(E,G,t);  !!n. n:nat ==> f(n) = t O r(n) |]==>mediating(E,G,r,f,t)"
  (fn prems => [safe_tac (!claset),trr prems 1]);
 
 val mediating_emb = prove_goalw Limit.thy [mediating_def]
diff -r 56544d061e1d -r e0baea4d485a src/ZF/ex/ListN.thy
--- a/src/ZF/ex/ListN.thy	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/ex/ListN.thy	Fri Oct 10 18:23:31 1997 +0200
@@ -16,5 +16,5 @@
   intrs
     NilI  "<0,Nil> : listn(A)"
     ConsI "[| a: A;  <n,l> : listn(A) |] ==> <succ(n), Cons(a,l)> : listn(A)"
-  type_intrs "nat_typechecks @ list.intrs"
+  type_intrs "nat_typechecks @ list. intrs"
 end
diff -r 56544d061e1d -r e0baea4d485a src/ZF/ex/Primrec.ML
--- a/src/ZF/ex/Primrec.ML	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/ex/Primrec.ML	Fri Oct 10 18:23:31 1997 +0200
@@ -137,7 +137,7 @@
 (*PROPERTY A 5', monotonicity for le *)
 goal Primrec.thy
     "!!i j k. [| j le k;  i: nat;  k:nat |] ==> ack(i,j) le ack(i,k)";
-by (res_inst_tac [("f", "%j.ack(i,j)")] Ord_lt_mono_imp_le_mono 1);
+by (res_inst_tac [("f", "%j. ack(i,j)")] Ord_lt_mono_imp_le_mono 1);
 by (REPEAT (ares_tac [ack_lt_mono2, ack_type RS nat_into_Ord] 1));
 qed "ack_le_mono2";
 
@@ -170,7 +170,7 @@
 (*PROPERTY A 7', monotonicity for le *)
 goal Primrec.thy
     "!!i j k. [| i le j; j:nat; k:nat |] ==> ack(i,k) le ack(j,k)";
-by (res_inst_tac [("f", "%j.ack(j,k)")] Ord_lt_mono_imp_le_mono 1);
+by (res_inst_tac [("f", "%j. ack(j,k)")] Ord_lt_mono_imp_le_mono 1);
 by (REPEAT (ares_tac [ack_lt_mono1, ack_type RS nat_into_Ord] 1));
 qed "ack_le_mono1";
 
diff -r 56544d061e1d -r e0baea4d485a src/ZF/ex/Primrec.thy
--- a/src/ZF/ex/Primrec.thy	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/ex/Primrec.thy	Fri Oct 10 18:23:31 1997 +0200
@@ -30,11 +30,11 @@
 
 defs
 
-  SC_def    "SC == lam l:list(nat).list_case(0, %x xs.succ(x), l)"
+  SC_def    "SC == lam l:list(nat).list_case(0, %x xs. succ(x), l)"
 
   CONST_def "CONST(k) == lam l:list(nat).k"
 
-  PROJ_def  "PROJ(i) == lam l:list(nat). list_case(0, %x xs.x, drop(i,l))"
+  PROJ_def  "PROJ(i) == lam l:list(nat). list_case(0, %x xs. x, drop(i,l))"
 
   COMP_def  "COMP(g,fs) == lam l:list(nat). g ` map(%f. f`l, fs)"
 
@@ -57,7 +57,7 @@
     PREC     "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"
   monos      "[list_mono]"
   con_defs   "[SC_def,CONST_def,PROJ_def,COMP_def,PREC_def]"
-  type_intrs "nat_typechecks @ list.intrs @                     
+  type_intrs "nat_typechecks @ list. intrs @                     
               [lam_type, list_case_type, drop_type, map_type,   
               apply_type, rec_type]"
 
diff -r 56544d061e1d -r e0baea4d485a src/ZF/ex/PropLog.thy
--- a/src/ZF/ex/PropLog.thy	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/ex/PropLog.thy	Fri Oct 10 18:23:31 1997 +0200
@@ -48,7 +48,7 @@
 
   prop_rec_def
    "prop_rec(p,b,c,h) == 
-   Vrec(p, %p g.prop_case(b, c, %x y. h(x, y, g`x, g`y), p))"
+   Vrec(p, %p g. prop_case(b, c, %x y. h(x, y, g`x, g`y), p))"
 
   (** Semantics of propositional logic **)
   is_true_def
diff -r 56544d061e1d -r e0baea4d485a src/ZF/ex/Rmap.thy
--- a/src/ZF/ex/Rmap.thy	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/ex/Rmap.thy	Fri Oct 10 18:23:31 1997 +0200
@@ -19,7 +19,7 @@
     ConsI "[| <x,y>: r;  <xs,ys> : rmap(r) |] ==> 
           <Cons(x,xs), Cons(y,ys)> : rmap(r)"
 
-  type_intrs "[domainI,rangeI] @ list.intrs"
+  type_intrs "[domainI,rangeI] @ list. intrs"
 
 end
   
diff -r 56544d061e1d -r e0baea4d485a src/ZF/ex/TF.ML
--- a/src/ZF/ex/TF.ML	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/ex/TF.ML	Fri Oct 10 18:23:31 1997 +0200
@@ -229,13 +229,13 @@
 
 (** theorems about TF_map **)
 
-goal TF.thy "!!z A. z: tree_forest(A) ==> TF_map(%u.u, z) = z";
+goal TF.thy "!!z A. z: tree_forest(A) ==> TF_map(%u. u, z) = z";
 by (etac tree_forest.induct 1);
 by (ALLGOALS Asm_simp_tac);
 qed "TF_map_ident";
 
 goal TF.thy
- "!!z A. z: tree_forest(A) ==> TF_map(h, TF_map(j,z)) = TF_map(%u.h(j(u)), z)";
+ "!!z A. z: tree_forest(A) ==> TF_map(h, TF_map(j,z)) = TF_map(%u. h(j(u)), z)";
 by (etac tree_forest.induct 1);
 by (ALLGOALS Asm_simp_tac);
 qed "TF_map_compose";
diff -r 56544d061e1d -r e0baea4d485a src/ZF/ex/TF.thy
--- a/src/ZF/ex/TF.thy	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/ex/TF.thy	Fri Oct 10 18:23:31 1997 +0200
@@ -37,13 +37,13 @@
     "TF_of_list(f) == list_rec(f, Fnil,  %t f r. Fcons(t,r))"
 
   TF_map_def
-    "TF_map(h,z) == TF_rec(z, %x f r.Tcons(h(x),r), Fnil, 
+    "TF_map(h,z) == TF_rec(z, %x f r. Tcons(h(x),r), Fnil, 
                            %t f r1 r2. Fcons(r1,r2))"
 
   TF_size_def
-    "TF_size(z) == TF_rec(z, %x f r.succ(r), 0, %t f r1 r2. r1#+r2)"
+    "TF_size(z) == TF_rec(z, %x f r. succ(r), 0, %t f r1 r2. r1#+r2)"
 
   TF_preorder_def
-    "TF_preorder(z) == TF_rec(z, %x f r.Cons(x,r), Nil, %t f r1 r2. r1@r2)"
+    "TF_preorder(z) == TF_rec(z, %x f r. Cons(x,r), Nil, %t f r1 r2. r1@r2)"
 
 end
diff -r 56544d061e1d -r e0baea4d485a src/ZF/ex/Term.ML
--- a/src/ZF/ex/Term.ML	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/ex/Term.ML	Fri Oct 10 18:23:31 1997 +0200
@@ -105,7 +105,7 @@
 
 val [rew,tslist] = goal Term.thy
     "[| !!t. j(t)==term_rec(t,d);  ts: list(A) |] ==> \
-\    j(Apply(a,ts)) = d(a, ts, map(%Z.j(Z), ts))";
+\    j(Apply(a,ts)) = d(a, ts, map(%Z. j(Z), ts))";
 by (rewtac rew);
 by (rtac (tslist RS term_rec) 1);
 qed "def_term_rec";
@@ -177,13 +177,13 @@
 
 (** theorems about term_map **)
 
-goal Term.thy "!!t A. t: term(A) ==> term_map(%u.u, t) = t";
+goal Term.thy "!!t A. t: term(A) ==> term_map(%u. u, t) = t";
 by (etac term_induct_eqn 1);
 by (asm_simp_tac (!simpset addsimps [map_ident]) 1);
 qed "term_map_ident";
 
 goal Term.thy
-  "!!t A. t: term(A) ==> term_map(f, term_map(g,t)) = term_map(%u.f(g(u)), t)";
+  "!!t A. t: term(A) ==> term_map(f, term_map(g,t)) = term_map(%u. f(g(u)), t)";
 by (etac term_induct_eqn 1);
 by (asm_simp_tac (!simpset addsimps [map_compose]) 1);
 qed "term_map_compose";
diff -r 56544d061e1d -r e0baea4d485a src/ZF/ex/Term.thy
--- a/src/ZF/ex/Term.thy	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/ex/Term.thy	Fri Oct 10 18:23:31 1997 +0200
@@ -29,7 +29,7 @@
 defs
   term_rec_def
    "term_rec(t,d) == 
-   Vrec(t, %t g. term_case(%x zs. d(x, zs, map(%z.g`z, zs)), t))"
+   Vrec(t, %t g. term_case(%x zs. d(x, zs, map(%z. g`z, zs)), t))"
 
   term_map_def  "term_map(f,t) == term_rec(t, %x zs rs. Apply(f(x), rs))"
 
diff -r 56544d061e1d -r e0baea4d485a src/ZF/func.ML
--- a/src/ZF/func.ML	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/func.ML	Fri Oct 10 18:23:31 1997 +0200
@@ -164,15 +164,15 @@
 qed "lamD";
 
 val prems = goalw ZF.thy [lam_def, Pi_def, function_def]
-    "[| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A.b(x)) : Pi(A,B)";  
+    "[| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A. b(x)) : Pi(A,B)";  
 by (blast_tac (!claset addIs prems) 1);
 qed "lam_type";
 
-goal ZF.thy "(lam x:A.b(x)) : A -> {b(x). x:A}";
+goal ZF.thy "(lam x:A. b(x)) : A -> {b(x). x:A}";
 by (REPEAT (ares_tac [refl,lam_type,RepFunI] 1));
 qed "lam_funtype";
 
-goal ZF.thy "!!a A. a : A ==> (lam x:A.b(x)) ` a = b(a)";
+goal ZF.thy "!!a A. a : A ==> (lam x:A. b(x)) ` a = b(a)";
 by (REPEAT (ares_tac [apply_equality,lam_funtype,lamI] 1));
 qed "beta";
 
@@ -230,7 +230,7 @@
 (*Every element of Pi(A,B) may be expressed as a lambda abstraction!*)
 val prems = goal ZF.thy
     "[| f: Pi(A,B);        \
-\       !!b. [| ALL x:A. b(x):B(x);  f = (lam x:A.b(x)) |] ==> P   \
+\       !!b. [| ALL x:A. b(x):B(x);  f = (lam x:A. b(x)) |] ==> P   \
 \    |] ==> P";
 by (resolve_tac prems 1);
 by (rtac (eta RS sym) 2);
@@ -240,7 +240,7 @@
 
 (** Images of functions **)
 
-goalw ZF.thy [lam_def] "!!C A. C <= A ==> (lam x:A.b(x)) `` C = {b(x). x:C}";
+goalw ZF.thy [lam_def] "!!C A. C <= A ==> (lam x:A. b(x)) `` C = {b(x). x:C}";
 by (Blast_tac 1);
 qed "image_lam";
 
diff -r 56544d061e1d -r e0baea4d485a src/ZF/mono.ML
--- a/src/ZF/mono.ML	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/mono.ML	Fri Oct 10 18:23:31 1997 +0200
@@ -178,13 +178,13 @@
 qed "imp_refl";
 
 val [PQimp] = goal IFOL.thy
-    "[| !!x. P(x) --> Q(x) |] ==> (EX x.P(x)) --> (EX x.Q(x))";
+    "[| !!x. P(x) --> Q(x) |] ==> (EX x. P(x)) --> (EX x. Q(x))";
 by IntPr.safe_tac;
 by (etac (PQimp RS mp RS exI) 1);
 qed "ex_mono";
 
 val [PQimp] = goal IFOL.thy
-    "[| !!x. P(x) --> Q(x) |] ==> (ALL x.P(x)) --> (ALL x.Q(x))";
+    "[| !!x. P(x) --> Q(x) |] ==> (ALL x. P(x)) --> (ALL x. Q(x))";
 by IntPr.safe_tac;
 by (etac (spec RS (PQimp RS mp)) 1);
 qed "all_mono";
diff -r 56544d061e1d -r e0baea4d485a src/ZF/pair.ML
--- a/src/ZF/pair.ML	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/pair.ML	Fri Oct 10 18:23:31 1997 +0200
@@ -131,7 +131,7 @@
 (*** Eliminator - split ***)
 
 (*A META-equality, so that it applies to higher types as well...*)
-qed_goalw "split" ZF.thy [split_def] "split(%x y.c(x,y), <a,b>) == c(a,b)"
+qed_goalw "split" ZF.thy [split_def] "split(%x y. c(x,y), <a,b>) == c(a,b)"
  (fn _ => [ (Simp_tac 1),
             (rtac reflexive_thm 1) ]);
 
@@ -140,7 +140,7 @@
 qed_goal "split_type" ZF.thy
     "[|  p:Sigma(A,B);   \
 \        !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x,y>) \
-\    |] ==> split(%x y.c(x,y), p) : C(p)"
+\    |] ==> split(%x y. c(x,y), p) : C(p)"
  (fn major::prems=>
   [ (rtac (major RS SigmaE) 1),
     (asm_simp_tac (!simpset addsimps prems) 1) ]);
diff -r 56544d061e1d -r e0baea4d485a src/ZF/simpdata.ML
--- a/src/ZF/simpdata.ML	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/simpdata.ML	Fri Oct 10 18:23:31 1997 +0200
@@ -20,8 +20,8 @@
      "(ALL x:A. P --> Q(x)) <-> (P --> (ALL x:A. Q(x)))",
      "(ALL x:A. P(x) --> Q) <-> ((EX x:A. P(x)) --> Q)",
      "(ALL x:0.P(x)) <-> True",
-     "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i.P(x))",
-     "(ALL x:cons(a,B).P(x)) <-> P(a) & (ALL x:B.P(x))",
+     "(ALL x:succ(i).P(x)) <-> P(i) & (ALL x:i. P(x))",
+     "(ALL x:cons(a,B).P(x)) <-> P(a) & (ALL x:B. P(x))",
      "(ALL x:RepFun(A,f). P(x)) <-> (ALL y:A. P(f(y)))",
      "(ALL x:Union(A).P(x)) <-> (ALL y:A. ALL x:y. P(x))",
      "(ALL x:Collect(A,Q).P(x)) <-> (ALL x:A. Q(x) --> P(x))"];
@@ -33,8 +33,8 @@
     ["(EX x:A. P(x) & Q) <-> ((EX x:A. P(x)) & Q)",
      "(EX x:A. P & Q(x)) <-> (P & (EX x:A. Q(x)))",
      "(EX x:0.P(x)) <-> False",
-     "(EX x:succ(i).P(x)) <-> P(i) | (EX x:i.P(x))",
-     "(EX x:cons(a,B).P(x)) <-> P(a) | (EX x:B.P(x))",
+     "(EX x:succ(i).P(x)) <-> P(i) | (EX x:i. P(x))",
+     "(EX x:cons(a,B).P(x)) <-> P(a) | (EX x:B. P(x))",
      "(EX x:RepFun(A,f). P(x)) <-> (EX y:A. P(f(y)))",
      "(EX x:Union(A).P(x)) <-> (EX y:A. EX x:y.  P(x))",
      "(EX x:Collect(A,Q).P(x)) <-> (EX x:A. Q(x) & P(x))"];
diff -r 56544d061e1d -r e0baea4d485a src/ZF/subset.ML
--- a/src/ZF/subset.ML	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/subset.ML	Fri Oct 10 18:23:31 1997 +0200
@@ -77,15 +77,15 @@
 qed "subset_UN_iff_eq";
 
 qed_goal "UN_subset_iff" ZF.thy
-     "(UN x:A.B(x)) <= C <-> (ALL x:A. B(x) <= C)"
+     "(UN x:A. B(x)) <= C <-> (ALL x:A. B(x) <= C)"
  (fn _ => [ Blast_tac 1 ]);
 
 qed_goal "UN_upper" ZF.thy
-    "!!x A. x:A ==> B(x) <= (UN x:A.B(x))"
+    "!!x A. x:A ==> B(x) <= (UN x:A. B(x))"
  (fn _ => [ etac (RepFunI RS Union_upper) 1 ]);
 
 qed_goal "UN_least" ZF.thy
-    "[| !!x. x:A ==> B(x)<=C |] ==> (UN x:A.B(x)) <= C"
+    "[| !!x. x:A ==> B(x)<=C |] ==> (UN x:A. B(x)) <= C"
  (fn [prem]=>
   [ (rtac (ballI RS (UN_subset_iff RS iffD2)) 1),
     (etac prem 1) ]);
@@ -109,11 +109,11 @@
 (*** Intersection of a family of sets  ***)
 
 qed_goal "INT_lower" ZF.thy
-    "!!x. x:A ==> (INT x:A.B(x)) <= B(x)"
+    "!!x. x:A ==> (INT x:A. B(x)) <= B(x)"
  (fn _ => [ Blast_tac 1 ]);
 
 qed_goal "INT_greatest" ZF.thy
-    "[| a:A;  !!x. x:A ==> C<=B(x) |] ==> C <= (INT x:A.B(x))"
+    "[| a:A;  !!x. x:A ==> C<=B(x) |] ==> C <= (INT x:A. B(x))"
  (fn [nonempty,prem] =>
   [ rtac (nonempty RS RepFunI RS Inter_greatest) 1,
     REPEAT (eresolve_tac [RepFunE, prem, ssubst] 1) ]);
diff -r 56544d061e1d -r e0baea4d485a src/ZF/upair.ML
--- a/src/ZF/upair.ML	Fri Oct 10 18:17:17 1997 +0200
+++ b/src/ZF/upair.ML	Fri Oct 10 18:23:31 1997 +0200
@@ -213,7 +213,7 @@
 
 (*Easier to apply than theI: conclusion has only one occurrence of P*)
 qed_goal "theI2" ZF.thy
-    "[| EX! x. P(x);  !!x. P(x) ==> Q(x) |] ==> Q(THE x.P(x))"
+    "[| EX! x. P(x);  !!x. P(x) ==> Q(x) |] ==> Q(THE x. P(x))"
  (fn prems => [ resolve_tac prems 1, 
                 rtac theI 1, 
                 resolve_tac prems 1 ]);