# HG changeset patch
# User wenzelm
# Date 876496212 -7200
# Node ID d7f033c74b38ede018101970b17b531b79112682
# Parent  f1a1817659e628cb255010593174ce987e8c0239
fixed dots;

diff -r f1a1817659e6 -r d7f033c74b38 src/CCL/CCL.ML
--- a/src/CCL/CCL.ML	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/CCL.ML	Fri Oct 10 17:10:12 1997 +0200
@@ -22,7 +22,7 @@
 qed_goal "arg_cong" CCL.thy "x=y ==> f(x)=f(y)"
  (fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]);
 
-goal CCL.thy  "(ALL x. f(x) = g(x)) --> (%x.f(x)) = (%x.g(x))";
+goal CCL.thy  "(ALL x. f(x) = g(x)) --> (%x. f(x)) = (%x. g(x))";
 by (simp_tac (CCL_ss addsimps [eq_iff]) 1);
 by (fast_tac (set_cs addIs [po_abstractn]) 1);
 bind_thm("abstractn", standard (allI RS (result() RS mp)));
@@ -68,7 +68,7 @@
 
 val ccl_injs = map (mk_inj_rl CCL.thy caseBs)
                ["<a,b> = <a',b'> <-> (a=a' & b=b')",
-                "(lam x.b(x) = lam x.b'(x)) <-> ((ALL z.b(z)=b'(z)))"];
+                "(lam x. b(x) = lam x. b'(x)) <-> ((ALL z. b(z)=b'(z)))"];
 
 val pair_inject = ((hd ccl_injs) RS iffD1) RS conjE;
 
@@ -140,13 +140,13 @@
 by (resolve_tac (prems RL [major RS ssubst]) 1);
 qed "XHlemma1";
 
-goal CCL.thy "(P(t,t') <-> Q) --> (<t,t'> : {p.EX t t'.p=<t,t'> &  P(t,t')} <-> Q)";
+goal CCL.thy "(P(t,t') <-> Q) --> (<t,t'> : {p. EX t t'. p=<t,t'> &  P(t,t')} <-> Q)";
 by (fast_tac ccl_cs 1);
 bind_thm("XHlemma2", result() RS mp);
 
 (*** Pre-Order ***)
 
-goalw CCL.thy [POgen_def,SIM_def]  "mono(%X.POgen(X))";
+goalw CCL.thy [POgen_def,SIM_def]  "mono(%X. POgen(X))";
 by (rtac monoI 1);
 by (safe_tac ccl_cs);
 by (REPEAT_SOME (resolve_tac [exI,conjI,refl]));
@@ -156,15 +156,15 @@
 
 goalw CCL.thy [POgen_def,SIM_def]
   "<t,t'> : POgen(R) <-> t= bot | (t=true & t'=true)  | (t=false & t'=false) | \
-\                    (EX a a' b b'.t=<a,b> &  t'=<a',b'>  & <a,a'> : R & <b,b'> : R) | \
-\                    (EX f f'.t=lam x.f(x) &  t'=lam x.f'(x) & (ALL x.<f(x),f'(x)> : R))";
+\                    (EX a a' b b'. t=<a,b> &  t'=<a',b'>  & <a,a'> : R & <b,b'> : R) | \
+\                    (EX f f'. t=lam x. f(x) &  t'=lam x. f'(x) & (ALL x. <f(x),f'(x)> : R))";
 by (rtac (iff_refl RS XHlemma2) 1);
 qed "POgenXH";
 
 goal CCL.thy
   "t [= t' <-> t=bot | (t=true & t'=true) | (t=false & t'=false) | \
-\                    (EX a a' b b'.t=<a,b> &  t'=<a',b'>  & a [= a' & b [= b') | \
-\                    (EX f f'.t=lam x.f(x) &  t'=lam x.f'(x) & (ALL x.f(x) [= f'(x)))";
+\                    (EX a a' b b'. t=<a,b> &  t'=<a',b'>  & a [= a' & b [= b') | \
+\                    (EX f f'. t=lam x. f(x) &  t'=lam x. f'(x) & (ALL x. f(x) [= f'(x)))";
 by (simp_tac (ccl_ss addsimps [PO_iff]) 1);
 br (rewrite_rule [POgen_def,SIM_def] 
                  (POgen_mono RS (PO_def RS def_gfp_Tarski) RS XHlemma1)) 1;
@@ -189,7 +189,7 @@
 by (fast_tac ccl_cs 1);
 qed "po_pair";
 
-goal CCL.thy "lam x.f(x) [= lam x.f'(x) <-> (ALL x. f(x) [= f'(x))";
+goal CCL.thy "lam x. f(x) [= lam x. f'(x) <-> (ALL x. f(x) [= f'(x))";
 by (rtac (poXH RS iff_trans) 1);
 by (simp_tac ccl_ss 1);
 by (REPEAT (ares_tac [iffI,allI] 1 ORELSE eresolve_tac [exE,conjE] 1));
@@ -200,13 +200,13 @@
 val ccl_porews = [po_bot,po_pair,po_lam];
 
 val [p1,p2,p3,p4,p5] = goal CCL.thy
-    "[| t [= t';  a [= a';  b [= b';  !!x y.c(x,y) [= c'(x,y); \
-\       !!u.d(u) [= d'(u) |] ==> case(t,a,b,c,d) [= case(t',a',b',c',d')";
+    "[| t [= t';  a [= a';  b [= b';  !!x y. c(x,y) [= c'(x,y); \
+\       !!u. d(u) [= d'(u) |] ==> case(t,a,b,c,d) [= case(t',a',b',c',d')";
 by (rtac (p1 RS po_cong RS po_trans) 1);
 by (rtac (p2 RS po_cong RS po_trans) 1);
 by (rtac (p3 RS po_cong RS po_trans) 1);
 by (rtac (p4 RS po_abstractn RS po_abstractn RS po_cong RS po_trans) 1);
-by (res_inst_tac [("f1","%d.case(t',a',b',c',d)")] 
+by (res_inst_tac [("f1","%d. case(t',a',b',c',d)")] 
                (p5 RS po_abstractn RS po_cong RS po_trans) 1);
 by (rtac po_refl 1);
 qed "case_pocong";
@@ -217,7 +217,7 @@
 qed "apply_pocong";
 
 
-val prems = goal CCL.thy "~ lam x.b(x) [= bot";
+val prems = goal CCL.thy "~ lam x. b(x) [= bot";
 by (rtac notI 1);
 by (dtac bot_poleast 1);
 by (etac (distinctness RS notE) 1);
@@ -230,14 +230,14 @@
 by (resolve_tac prems 1);
 qed "po_lemma";
 
-goal CCL.thy "~ <a,b> [= lam x.f(x)";
+goal CCL.thy "~ <a,b> [= lam x. f(x)";
 by (rtac notI 1);
 by (rtac (npo_lam_bot RS notE) 1);
 by (etac (case_pocong RS (caseBlam RS (caseBpair RS po_lemma))) 1);
 by (REPEAT (resolve_tac [po_refl,npo_lam_bot] 1));
 qed "npo_pair_lam";
 
-goal CCL.thy "~ lam x.f(x) [= <a,b>";
+goal CCL.thy "~ lam x. f(x) [= <a,b>";
 by (rtac notI 1);
 by (rtac (npo_lam_bot RS notE) 1);
 by (etac (case_pocong RS (caseBpair RS (caseBlam RS po_lemma))) 1);
@@ -252,9 +252,9 @@
 val npo_rls = [npo_pair_lam,npo_lam_pair] @ map mk_thm
             ["~ true [= false",          "~ false [= true",
              "~ true [= <a,b>",          "~ <a,b> [= true",
-             "~ true [= lam x.f(x)","~ lam x.f(x) [= true",
+             "~ true [= lam x. f(x)","~ lam x. f(x) [= true",
             "~ false [= <a,b>",          "~ <a,b> [= false",
-            "~ false [= lam x.f(x)","~ lam x.f(x) [= false"];
+            "~ false [= lam x. f(x)","~ lam x. f(x) [= false"];
 
 (* Coinduction for [= *)
 
@@ -267,7 +267,7 @@
 
 (*************** EQUALITY *******************)
 
-goalw CCL.thy [EQgen_def,SIM_def]  "mono(%X.EQgen(X))";
+goalw CCL.thy [EQgen_def,SIM_def]  "mono(%X. EQgen(X))";
 by (rtac monoI 1);
 by (safe_tac set_cs);
 by (REPEAT_SOME (resolve_tac [exI,conjI,refl]));
@@ -278,19 +278,19 @@
 goalw CCL.thy [EQgen_def,SIM_def]
   "<t,t'> : EQgen(R) <-> (t=bot & t'=bot)  | (t=true & t'=true)  | \
 \                                            (t=false & t'=false) | \
-\                (EX a a' b b'.t=<a,b> &  t'=<a',b'>  & <a,a'> : R & <b,b'> : R) | \
-\                (EX f f'.t=lam x.f(x) &  t'=lam x.f'(x) & (ALL x.<f(x),f'(x)> : R))";
+\                (EX a a' b b'. t=<a,b> &  t'=<a',b'>  & <a,a'> : R & <b,b'> : R) | \
+\                (EX f f'. t=lam x. f(x) &  t'=lam x. f'(x) & (ALL x.<f(x),f'(x)> : R))";
 by (rtac (iff_refl RS XHlemma2) 1);
 qed "EQgenXH";
 
 goal CCL.thy
   "t=t' <-> (t=bot & t'=bot)  | (t=true & t'=true)  | (t=false & t'=false) | \
-\                    (EX a a' b b'.t=<a,b> &  t'=<a',b'>  & a=a' & b=b') | \
-\                    (EX f f'.t=lam x.f(x) &  t'=lam x.f'(x) & (ALL x.f(x)=f'(x)))";
+\                    (EX a a' b b'. t=<a,b> &  t'=<a',b'>  & a=a' & b=b') | \
+\                    (EX f f'. t=lam x. f(x) &  t'=lam x. f'(x) & (ALL x. f(x)=f'(x)))";
 by (subgoal_tac
   "<t,t'> : EQ <-> (t=bot & t'=bot)  | (t=true & t'=true) | (t=false & t'=false) | \
-\             (EX a a' b b'.t=<a,b> &  t'=<a',b'>  & <a,a'> : EQ & <b,b'> : EQ) | \
-\             (EX f f'.t=lam x.f(x) &  t'=lam x.f'(x) & (ALL x.<f(x),f'(x)> : EQ))" 1);
+\             (EX a a' b b'. t=<a,b> &  t'=<a',b'>  & <a,a'> : EQ & <b,b'> : EQ) | \
+\             (EX f f'. t=lam x. f(x) &  t'=lam x. f'(x) & (ALL x. <f(x),f'(x)> : EQ))" 1);
 by (etac rev_mp 1);
 by (simp_tac (CCL_ss addsimps [EQ_iff RS iff_sym]) 1);
 br (rewrite_rule [EQgen_def,SIM_def]
@@ -304,7 +304,7 @@
 qed "eq_coinduct";
 
 val prems = goal CCL.thy 
-    "[|  <t,u> : R;  R <= EQgen(lfp(%x.EQgen(x) Un R Un EQ)) |] ==> t = u";
+    "[|  <t,u> : R;  R <= EQgen(lfp(%x. EQgen(x) Un R Un EQ)) |] ==> t = u";
 by (rtac (EQ_def RS def_coinduct3 RS (EQ_iff RS iffD2)) 1);
 by (REPEAT (ares_tac (EQgen_mono::prems) 1));
 qed "eq_coinduct3";
@@ -314,18 +314,18 @@
 
 (*** Untyped Case Analysis and Other Facts ***)
 
-goalw CCL.thy [apply_def]  "(EX f.t=lam x.f(x)) --> t = lam x.(t ` x)";
+goalw CCL.thy [apply_def]  "(EX f. t=lam x. f(x)) --> t = lam x.(t ` x)";
 by (safe_tac ccl_cs);
 by (simp_tac ccl_ss 1);
 bind_thm("cond_eta", result() RS mp);
 
-goal CCL.thy "(t=bot) | (t=true) | (t=false) | (EX a b.t=<a,b>) | (EX f.t=lam x.f(x))";
+goal CCL.thy "(t=bot) | (t=true) | (t=false) | (EX a b. t=<a,b>) | (EX f. t=lam x. f(x))";
 by (cut_facts_tac [refl RS (eqXH RS iffD1)] 1);
 by (fast_tac set_cs 1);
 qed "exhaustion";
 
 val prems = goal CCL.thy 
-    "[| P(bot);  P(true);  P(false);  !!x y.P(<x,y>);  !!b.P(lam x.b(x)) |] ==> P(t)";
+    "[| P(bot);  P(true);  P(false);  !!x y. P(<x,y>);  !!b. P(lam x. b(x)) |] ==> P(t)";
 by (cut_facts_tac [exhaustion] 1);
 by (REPEAT_SOME (ares_tac prems ORELSE' eresolve_tac [disjE,exE,ssubst]));
 qed "term_case";
diff -r f1a1817659e6 -r d7f033c74b38 src/CCL/CCL.thy
--- a/src/CCL/CCL.thy	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/CCL.thy	Fri Oct 10 17:10:12 1997 +0200
@@ -56,18 +56,18 @@
   trueV       "true ---> true"
   falseV      "false ---> false"
   pairV       "<a,b> ---> <a,b>"
-  lamV        "lam x.b(x) ---> lam x.b(x)"
+  lamV        "lam x. b(x) ---> lam x. b(x)"
   caseVtrue   "[| t ---> true;  d ---> c |] ==> case(t,d,e,f,g) ---> c"
   caseVfalse  "[| t ---> false;  e ---> c |] ==> case(t,d,e,f,g) ---> c"
   caseVpair   "[| t ---> <a,b>;  f(a,b) ---> c |] ==> case(t,d,e,f,g) ---> c"
-  caseVlam    "[| t ---> lam x.b(x);  g(b) ---> c |] ==> case(t,d,e,f,g) ---> c"
+  caseVlam    "[| t ---> lam x. b(x);  g(b) ---> c |] ==> case(t,d,e,f,g) ---> c"
 
   (*** Properties of evaluation: note that "t ---> c" impies that c is canonical ***)
 
   canonical  "[| t ---> c; c==true ==> u--->v; 
                           c==false ==> u--->v; 
-                    !!a b.c==<a,b> ==> u--->v; 
-                      !!f.c==lam x.f(x) ==> u--->v |] ==> 
+                    !!a b. c==<a,b> ==> u--->v; 
+                      !!f. c==lam x. f(x) ==> u--->v |] ==> 
              u--->v"
 
   (* Should be derivable - but probably a bitch! *)
@@ -77,9 +77,9 @@
 
   (*** Definitions used in the following rules ***)
 
-  apply_def     "f ` t == case(f,bot,bot,%x y.bot,%u.u(t))"
-  bot_def         "bot == (lam x.x`x)`(lam x.x`x)"
-  fix_def      "fix(f) == (lam x.f(x`x))`(lam x.f(x`x))"
+  apply_def     "f ` t == case(f,bot,bot,%x y. bot,%u. u(t))"
+  bot_def         "bot == (lam x. x`x)`(lam x. x`x)"
+  fix_def      "fix(f) == (lam x. f(x`x))`(lam x. f(x`x))"
 
   (*  The pre-order ([=) is defined as a simulation, and behavioural equivalence (=) *)
   (*  as a bisimulation.  They can both be expressed as (bi)simulations up to        *)
@@ -87,8 +87,8 @@
 
   SIM_def
   "SIM(t,t',R) ==  (t=true & t'=true) | (t=false & t'=false) | 
-                  (EX a a' b b'.t=<a,b> & t'=<a',b'> & <a,a'> : R & <b,b'> : R) | 
-                  (EX f f'.t=lam x.f(x) & t'=lam x.f'(x) & (ALL x.<f(x),f'(x)> : R))"
+                  (EX a a' b b'. t=<a,b> & t'=<a',b'> & <a,a'> : R & <b,b'> : R) | 
+                  (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x.<f(x),f'(x)> : R))"
 
   POgen_def  "POgen(R) == {p. EX t t'. p=<t,t'> & (t = bot | SIM(t,t',R))}"
   EQgen_def  "EQgen(R) == {p. EX t t'. p=<t,t'> & (t = bot & t' = bot | SIM(t,t',R))}"
@@ -105,7 +105,7 @@
   po_cong        "a [= b ==> f(a) [= f(b)"
 
   (* Extend definition of [= to program fragments of higher type *)
-  po_abstractn   "(!!x. f(x) [= g(x)) ==> (%x.f(x)) [= (%x.g(x))"
+  po_abstractn   "(!!x. f(x) [= g(x)) ==> (%x. f(x)) [= (%x. g(x))"
 
   (** Equality - equivalence axioms inherited from FOL.thy   **)
   (**          - congruence of "=" is axiomatised implicitly **)
@@ -122,11 +122,11 @@
   caseBtrue            "case(true,d,e,f,g) = d"
   caseBfalse          "case(false,d,e,f,g) = e"
   caseBpair           "case(<a,b>,d,e,f,g) = f(a,b)"
-  caseBlam       "case(lam x.b(x),d,e,f,g) = g(b)"
+  caseBlam       "case(lam x. b(x),d,e,f,g) = g(b)"
   caseBbot              "case(bot,d,e,f,g) = bot"            (* strictness *)
 
   (** The theory is non-trivial **)
-  distinctness   "~ lam x.b(x) = bot"
+  distinctness   "~ lam x. b(x) = bot"
 
   (*** Definitions of Termination and Divergence ***)
 
diff -r f1a1817659e6 -r d7f033c74b38 src/CCL/Fix.ML
--- a/src/CCL/Fix.ML	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/Fix.ML	Fri Oct 10 17:10:12 1997 +0200
@@ -11,7 +11,7 @@
 (*** Fixed Point Induction ***)
 
 val [base,step,incl] = goalw Fix.thy [INCL_def]
-    "[| P(bot);  !!x.P(x) ==> P(f(x));  INCL(P) |] ==> P(fix(f))";
+    "[| P(bot);  !!x. P(x) ==> P(f(x));  INCL(P) |] ==> P(fix(f))";
 by (rtac (incl RS spec RS mp) 1);
 by (rtac (Nat_ind RS ballI) 1 THEN atac 1);
 by (ALLGOALS (simp_tac term_ss));
@@ -26,18 +26,18 @@
 qed "inclXH";
 
 val prems = goal Fix.thy
-     "[| !!f.ALL n:Nat.P(f^n`bot) ==> P(fix(f)) |] ==> INCL(%x.P(x))";
+     "[| !!f. ALL n:Nat. P(f^n`bot) ==> P(fix(f)) |] ==> INCL(%x. P(x))";
 by (fast_tac (term_cs addIs (prems @ [XH_to_I inclXH])) 1);
 qed "inclI";
 
 val incl::prems = goal Fix.thy
-     "[| INCL(P);  !!n.n:Nat ==> P(f^n`bot) |] ==> P(fix(f))";
+     "[| INCL(P);  !!n. n:Nat ==> P(f^n`bot) |] ==> P(fix(f))";
 by (fast_tac (term_cs addIs ([ballI RS (incl RS (XH_to_D inclXH) RS spec RS mp)] 
                        @ prems)) 1);
 qed "inclD";
 
 val incl::prems = goal Fix.thy
-     "[| INCL(P);  (ALL n:Nat.P(f^n`bot))-->P(fix(f)) ==> R |] ==> R";
+     "[| INCL(P);  (ALL n:Nat. P(f^n`bot))-->P(fix(f)) ==> R |] ==> R";
 by (fast_tac (term_cs addIs ([incl RS inclD] @ prems)) 1);
 qed "inclE";
 
@@ -55,19 +55,19 @@
 by (rtac po_cong 1 THEN rtac po_bot 1);
 qed "npo_INCL";
 
-val prems = goal Fix.thy "[| INCL(P);  INCL(Q) |] ==> INCL(%x.P(x) & Q(x))";
+val prems = goal Fix.thy "[| INCL(P);  INCL(Q) |] ==> INCL(%x. P(x) & Q(x))";
 by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);;
 qed "conj_INCL";
 
-val prems = goal Fix.thy "[| !!a.INCL(P(a)) |] ==> INCL(%x.ALL a.P(a,x))";
+val prems = goal Fix.thy "[| !!a. INCL(P(a)) |] ==> INCL(%x. ALL a. P(a,x))";
 by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);;
 qed "all_INCL";
 
-val prems = goal Fix.thy "[| !!a.a:A ==> INCL(P(a)) |] ==> INCL(%x.ALL a:A.P(a,x))";
+val prems = goal Fix.thy "[| !!a. a:A ==> INCL(P(a)) |] ==> INCL(%x. ALL a:A. P(a,x))";
 by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);;
 qed "ball_INCL";
 
-goal Fix.thy "INCL(%x.a(x) = (b(x)::'a::prog))";
+goal Fix.thy "INCL(%x. a(x) = (b(x)::'a::prog))";
 by (simp_tac (term_ss addsimps [eq_iff]) 1);
 by (REPEAT (resolve_tac [conj_INCL,po_INCL] 1));
 qed "eq_INCL";
@@ -80,7 +80,7 @@
 by (rtac (fixB RS sym) 1);
 qed "fix_idgenfp";
 
-goalw Fix.thy [idgen_def] "idgen(lam x.x) = lam x.x";
+goalw Fix.thy [idgen_def] "idgen(lam x. x) = lam x. x";
 by (simp_tac term_ss 1);
 by (rtac (term_case RS allI) 1);
 by (ALLGOALS (simp_tac term_ss));
@@ -109,14 +109,14 @@
                "idgen(d) = d ==> d ` true = true",
                "idgen(d) = d ==> d ` false = false",
                "idgen(d) = d ==> d ` <a,b> = <d ` a,d ` b>",
-               "idgen(d) = d ==> d ` (lam x.f(x)) = lam x.d ` f(x)"]
+               "idgen(d) = d ==> d ` (lam x. f(x)) = lam x. d ` f(x)"]
     end;
 
 (* Proof of Reachability law - show that fix and lam x.x both give LEAST fixed points 
                                of idgen and hence are they same *)
 
 val [p1,p2,p3] = goal CCL.thy
-    "[| ALL x.t ` x [= u ` x;  EX f.t=lam x.f(x);  EX f.u=lam x.f(x) |] ==> t [= u";
+    "[| ALL x. t ` x [= u ` x;  EX f. t=lam x. f(x);  EX f. u=lam x. f(x) |] ==> t [= u";
 by (stac (p2 RS cond_eta) 1);
 by (stac (p3 RS cond_eta) 1);
 by (rtac (p1 RS (po_lam RS iffD2)) 1);
@@ -129,8 +129,8 @@
 
 val [prem] = goal Fix.thy
     "idgen(d) = d ==> \
-\      {p.EX a b.p=<a,b> & (EX t.a=fix(idgen) ` t & b = d ` t)} <=   \
-\      POgen({p.EX a b.p=<a,b> & (EX t.a=fix(idgen) ` t  & b = d ` t)})";
+\      {p. EX a b. p=<a,b> & (EX t. a=fix(idgen) ` t & b = d ` t)} <=   \
+\      POgen({p. EX a b. p=<a,b> & (EX t. a=fix(idgen) ` t  & b = d ` t)})";
 by (REPEAT (step_tac term_cs 1));
 by (term_case_tac "t" 1);
 by (ALLGOALS (simp_tac (term_ss addsimps (POgenXH::([prem,fix_idgenfp] RL idgen_lemmas)))));
@@ -146,7 +146,7 @@
 
 val [prem] = goal Fix.thy
     "idgen(d) = d ==> \
-\      {p.EX a b.p=<a,b> & b = d ` a} <= POgen({p.EX a b.p=<a,b> & b = d ` a})";
+\      {p. EX a b. p=<a,b> & b = d ` a} <= POgen({p. EX a b. p=<a,b> & b = d ` a})";
 by (REPEAT (step_tac term_cs 1));
 by (term_case_tac "a" 1);
 by (ALLGOALS (simp_tac (term_ss addsimps (POgenXH::([prem] RL idgen_lemmas)))));
@@ -154,14 +154,14 @@
 qed "lemma2";
 
 val [prem] = goal Fix.thy
-    "idgen(d) = d ==> lam x.x [= d";
+    "idgen(d) = d ==> lam x. x [= d";
 by (rtac (allI RS po_eta) 1);
 by (rtac (lemma2 RSN(2,po_coinduct)) 1);
 by (simp_tac term_ss 1);
 by (ALLGOALS (fast_tac (term_cs addIs [prem,po_eta_lemma,fix_idgenfp])));
 qed "id_least_idgen";
 
-goal Fix.thy  "fix(idgen) = lam x.x";
+goal Fix.thy  "fix(idgen) = lam x. x";
 by (fast_tac (term_cs addIs [eq_iff RS iffD2,
                              id_idgenfp RS fix_least_idgen,
                              fix_idgenfp RS id_least_idgen]) 1);
@@ -169,7 +169,7 @@
 
 (********)
 
-val [prem] = goal Fix.thy "f = lam x.x ==> f`t = t";
+val [prem] = goal Fix.thy "f = lam x. x ==> f`t = t";
 by (rtac (prem RS sym RS subst) 1);
 by (rtac applyB 1);
 qed "id_apply";
@@ -177,7 +177,7 @@
 val prems = goal Fix.thy
      "[| P(bot);  P(true);  P(false);  \
 \        !!x y.[| P(x);  P(y) |] ==> P(<x,y>);  \
-\        !!u.(!!x.P(u(x))) ==> P(lam x.u(x));  INCL(P) |] ==> \
+\        !!u.(!!x. P(u(x))) ==> P(lam x. u(x));  INCL(P) |] ==> \
 \     P(t)";
 by (rtac (reachability RS id_apply RS subst) 1);
 by (res_inst_tac [("x","t")] spec 1);
diff -r f1a1817659e6 -r d7f033c74b38 src/CCL/Fix.thy
--- a/src/CCL/Fix.thy	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/Fix.thy	Fri Oct 10 17:10:12 1997 +0200
@@ -17,10 +17,10 @@
 rules
 
   idgen_def
-  "idgen(f) == lam t.case(t,true,false,%x y.<f`x, f`y>,%u.lam x.f ` u(x))"
+  "idgen(f) == lam t. case(t,true,false,%x y.<f`x, f`y>,%u. lam x. f ` u(x))"
 
-  INCL_def   "INCL(%x.P(x)) == (ALL f.(ALL n:Nat.P(f^n`bot)) --> P(fix(f)))"
-  po_INCL    "INCL(%x.a(x) [= b(x))"
-  INCL_subst "INCL(P) ==> INCL(%x.P((g::i=>i)(x)))"
+  INCL_def   "INCL(%x. P(x)) == (ALL f.(ALL n:Nat. P(f^n`bot)) --> P(fix(f)))"
+  po_INCL    "INCL(%x. a(x) [= b(x))"
+  INCL_subst "INCL(P) ==> INCL(%x. P((g::i=>i)(x)))"
 
 end
diff -r f1a1817659e6 -r d7f033c74b38 src/CCL/Gfp.ML
--- a/src/CCL/Gfp.ML	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/Gfp.ML	Fri Oct 10 17:10:12 1997 +0200
@@ -71,13 +71,13 @@
          - instead of the condition  A <= f(A)
                            consider  A <= (f(A) Un f(f(A)) ...) Un gfp(A) ***)
 
-val [prem] = goal Gfp.thy "mono(f) ==> mono(%x.f(x) Un A Un B)";
+val [prem] = goal Gfp.thy "mono(f) ==> mono(%x. f(x) Un A Un B)";
 by (REPEAT (ares_tac [subset_refl, monoI, Un_mono, prem RS monoD] 1));
 qed "coinduct3_mono_lemma";
 
 val [prem,mono] = goal Gfp.thy
-    "[| A <= f(lfp(%x.f(x) Un A Un gfp(f)));  mono(f) |] ==> \
-\    lfp(%x.f(x) Un A Un gfp(f)) <= f(lfp(%x.f(x) Un A Un gfp(f)))";
+    "[| A <= f(lfp(%x. f(x) Un A Un gfp(f)));  mono(f) |] ==> \
+\    lfp(%x. f(x) Un A Un gfp(f)) <= f(lfp(%x. f(x) Un A Un gfp(f)))";
 by (rtac subset_trans 1);
 by (rtac (mono RS coinduct3_mono_lemma RS lfp_lemma3) 1);
 by (rtac (Un_least RS Un_least) 1);
@@ -90,7 +90,7 @@
 qed "coinduct3_lemma";
 
 val ainA::prems = goal Gfp.thy
-    "[| a:A;  A <= f(lfp(%x.f(x) Un A Un gfp(f))); mono(f) |] ==> a : gfp(f)";
+    "[| a:A;  A <= f(lfp(%x. f(x) Un A Un gfp(f))); mono(f) |] ==> a : gfp(f)";
 by (rtac coinduct 1);
 by (rtac (prems MRS coinduct3_lemma) 2);
 by (resolve_tac (prems RL [coinduct3_mono_lemma RS lfp_Tarski RS ssubst]) 1);
@@ -118,7 +118,7 @@
 qed "def_coinduct2";
 
 val rew::prems = goal Gfp.thy
-    "[| h==gfp(f);  a:A;  A <= f(lfp(%x.f(x) Un A Un h)); mono(f) |] ==> a: h";
+    "[| h==gfp(f);  a:A;  A <= f(lfp(%x. f(x) Un A Un h)); mono(f) |] ==> a: h";
 by (rewtac rew);
 by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems @ [coinduct3]) 1));
 qed "def_coinduct3";
diff -r f1a1817659e6 -r d7f033c74b38 src/CCL/Hered.ML
--- a/src/CCL/Hered.ML	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/Hered.ML	Fri Oct 10 17:10:12 1997 +0200
@@ -12,20 +12,20 @@
 
 (*** Hereditary Termination ***)
 
-goalw Hered.thy [HTTgen_def]  "mono(%X.HTTgen(X))";
+goalw Hered.thy [HTTgen_def]  "mono(%X. HTTgen(X))";
 by (rtac monoI 1);
 by (fast_tac set_cs 1);
 qed "HTTgen_mono";
 
 goalw Hered.thy [HTTgen_def]
-  "t : HTTgen(A) <-> t=true | t=false | (EX a b.t=<a,b> & a : A & b : A) | \
-\                                       (EX f.t=lam x.f(x) & (ALL x.f(x) : A))";
+  "t : HTTgen(A) <-> t=true | t=false | (EX a b. t=<a,b> & a : A & b : A) | \
+\                                       (EX f. t=lam x. f(x) & (ALL x. f(x) : A))";
 by (fast_tac set_cs 1);
 qed "HTTgenXH";
 
 goal Hered.thy
-  "t : HTT <-> t=true | t=false | (EX a b.t=<a,b> & a : HTT & b : HTT) | \
-\                                  (EX f.t=lam x.f(x) & (ALL x.f(x) : HTT))";
+  "t : HTT <-> t=true | t=false | (EX a b. t=<a,b> & a : HTT & b : HTT) | \
+\                                  (EX f. t=lam x. f(x) & (ALL x. f(x) : HTT))";
 br (rewrite_rule [HTTgen_def] 
                  (HTTgen_mono RS (HTT_def RS def_gfp_Tarski) RS XHlemma1)) 1;
 by (fast_tac set_cs 1);
@@ -50,7 +50,7 @@
 by (fast_tac term_cs 1);
 qed "HTT_pair";
 
-goal Hered.thy "lam x.f(x) : HTT <-> (ALL x. f(x) : HTT)";
+goal Hered.thy "lam x. f(x) : HTT <-> (ALL x. f(x) : HTT)";
 by (rtac (HTTXH RS iff_trans) 1);
 by (simp_tac term_ss 1);
 by (safe_tac term_cs);
@@ -97,7 +97,7 @@
        ["true : HTTgen(R)",
         "false : HTTgen(R)",
         "[| a : R;  b : R |] ==> <a,b> : HTTgen(R)",
-        "[| !!x. b(x) : R |] ==> lam x.b(x) : HTTgen(R)",
+        "[| !!x. b(x) : R |] ==> lam x. b(x) : HTTgen(R)",
         "one : HTTgen(R)",
         "a : lfp(%x. HTTgen(x) Un R Un HTT) ==> \
 \                         inl(a) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
@@ -127,7 +127,7 @@
 qed "PlusF";
 
 val prems = goal Hered.thy 
-     "[| A <= HTT;  !!x.x:A ==> B(x) <= HTT |] ==> SUM x:A.B(x) <= HTT";
+     "[| A <= HTT;  !!x. x:A ==> B(x) <= HTT |] ==> SUM x:A. B(x) <= HTT";
 by (simp_tac (CCL_ss addsimps ([subsetXH,SgXH] @ HTT_rews)) 1);
 by (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])) 1);
 qed "SigmaF";
@@ -178,7 +178,7 @@
 (*** but it seems as easy (and more general) to do this directly by coinduction ***)
 (*
 val prems = goal Hered.thy "[| t : HTT;  t [= u |] ==> u [= t";
-by (po_coinduct_tac "{p. EX a b.p=<a,b> & b : HTT & b [= a}" 1);
+by (po_coinduct_tac "{p. EX a b. p=<a,b> & b : HTT & b [= a}" 1);
 by (fast_tac (ccl_cs addIs prems) 1);
 by (safe_tac ccl_cs);
 by (dtac (poXH RS iffD1) 1);
diff -r f1a1817659e6 -r d7f033c74b38 src/CCL/Hered.thy
--- a/src/CCL/Hered.thy	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/Hered.thy	Fri Oct 10 17:10:12 1997 +0200
@@ -23,8 +23,8 @@
   (*** Definitions of Hereditary Termination ***)
 
   HTTgen_def 
-  "HTTgen(R) == {t. t=true | t=false | (EX a b.t=<a,b>      & a : R & b : R) | 
-                                      (EX f.  t=lam x.f(x) & (ALL x.f(x) : R))}"
+  "HTTgen(R) == {t. t=true | t=false | (EX a b. t=<a,b>      & a : R & b : R) | 
+                                      (EX f.  t=lam x. f(x) & (ALL x. f(x) : R))}"
   HTT_def       "HTT == gfp(HTTgen)"
 
 end
diff -r f1a1817659e6 -r d7f033c74b38 src/CCL/Lfp.ML
--- a/src/CCL/Lfp.ML	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/Lfp.ML	Fri Oct 10 17:10:12 1997 +0200
@@ -45,7 +45,7 @@
 
 val [lfp,mono,indhyp] = goal Lfp.thy
     "[| a: lfp(f);  mono(f);                            \
-\       !!x. [| x: f(lfp(f) Int {x.P(x)}) |] ==> P(x)   \
+\       !!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)   \
 \    |] ==> P(a)";
 by (res_inst_tac [("a","a")] (Int_lower2 RS subsetD RS CollectD) 1);
 by (rtac (lfp RSN (2, lfp_lowerbound RS subsetD)) 1);
@@ -64,7 +64,7 @@
 
 val rew::prems = goal Lfp.thy
     "[| A == lfp(f);  a:A;  mono(f);                    \
-\       !!x. [| x: f(A Int {x.P(x)}) |] ==> P(x)        \
+\       !!x. [| x: f(A Int {x. P(x)}) |] ==> P(x)        \
 \    |] ==> P(a)";
 by (EVERY1 [rtac induct,        (*backtracking to force correct induction*)
             REPEAT1 o (ares_tac (map (rewrite_rule [rew]) prems))]);
diff -r f1a1817659e6 -r d7f033c74b38 src/CCL/Set.ML
--- a/src/CCL/Set.ML	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/Set.ML	Fri Oct 10 17:10:12 1997 +0200
@@ -13,12 +13,12 @@
 
 open Set;
 
-val [prem] = goal Set.thy "[| P(a) |] ==> a : {x.P(x)}";
+val [prem] = goal Set.thy "[| P(a) |] ==> a : {x. P(x)}";
 by (rtac (mem_Collect_iff RS iffD2) 1);
 by (rtac prem 1);
 qed "CollectI";
 
-val prems = goal Set.thy "[| a : {x.P(x)} |] ==> P(a)";
+val prems = goal Set.thy "[| a : {x. P(x)} |] ==> P(a)";
 by (resolve_tac (prems RL [mem_Collect_iff  RS iffD1]) 1);
 qed "CollectD";
 
@@ -56,7 +56,7 @@
 qed "bexI";
 
 qed_goal "bexCI" Set.thy 
-   "[| EX x:A. ~P(x) ==> P(a);  a:A |] ==> EX x:A.P(x)"
+   "[| EX 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))  ]);
@@ -93,7 +93,7 @@
 
 (*** Rules for subsets ***)
 
-val prems = goalw Set.thy [subset_def] "(!!x.x:A ==> x:B) ==> A <= B";
+val prems = goalw Set.thy [subset_def] "(!!x. x:A ==> x:B) ==> A <= B";
 by (REPEAT (ares_tac (prems @ [ballI]) 1));
 qed "subsetI";
 
@@ -163,7 +163,7 @@
 by (REPEAT (resolve_tac (refl::prems) 1));
 qed "setup_induction";
 
-goal Set.thy "{x.x:A} = A";
+goal Set.thy "{x. x:A} = A";
 by (REPEAT (ares_tac [equalityI,subsetI,CollectI] 1  ORELSE etac CollectD 1));
 qed "trivial_set";
 
@@ -234,7 +234,7 @@
 
 (*** Empty sets ***)
 
-goalw Set.thy [empty_def] "{x.False} = {}";
+goalw Set.thy [empty_def] "{x. False} = {}";
 by (rtac refl 1);
 qed "empty_eq";
 
@@ -244,7 +244,7 @@
 
 val emptyE = make_elim emptyD;
 
-val [prem] = goal Set.thy "~ A={} ==> (EX x.x:A)";
+val [prem] = goal Set.thy "~ A={} ==> (EX x. x:A)";
 by (rtac (prem RS swap) 1);
 by (rtac equalityI 1);
 by (ALLGOALS (fast_tac (FOL_cs addSIs [subsetI] addSEs [emptyD])));
diff -r f1a1817659e6 -r d7f033c74b38 src/CCL/Set.thy
--- a/src/CCL/Set.thy	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/Set.thy	Fri Oct 10 17:10:12 1997 +0200
@@ -50,17 +50,17 @@
 
 
 rules
-  mem_Collect_iff       "(a : {x.P(x)}) <-> P(a)"
-  set_extension         "A=B <-> (ALL x.x:A <-> x:B)"
+  mem_Collect_iff       "(a : {x. P(x)}) <-> P(a)"
+  set_extension         "A=B <-> (ALL x. x:A <-> x:B)"
 
   Ball_def      "Ball(A, P)  == ALL x. x:A --> P(x)"
   Bex_def       "Bex(A, P)   == EX x. x:A & P(x)"
   mono_def      "mono(f)     == (ALL A B. A <= B --> f(A) <= f(B))"
   subset_def    "A <= B      == ALL x:A. x:B"
-  singleton_def "{a}         == {x.x=a}"
-  empty_def     "{}          == {x.False}"
-  Un_def        "A Un B      == {x.x:A | x:B}"
-  Int_def       "A Int B     == {x.x:A & x:B}"
+  singleton_def "{a}         == {x. x=a}"
+  empty_def     "{}          == {x. False}"
+  Un_def        "A Un B      == {x. x:A | x:B}"
+  Int_def       "A Int B     == {x. x:A & x:B}"
   Compl_def     "Compl(A)    == {x. ~x:A}"
   INTER_def     "INTER(A, B) == {y. ALL x:A. y: B(x)}"
   UNION_def     "UNION(A, B) == {y. EX x:A. y: B(x)}"
diff -r f1a1817659e6 -r d7f033c74b38 src/CCL/Term.ML
--- a/src/CCL/Term.ML	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/Term.ML	Fri Oct 10 17:10:12 1997 +0200
@@ -35,7 +35,7 @@
 by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam])));
 qed "letBbbot";
 
-goalw Term.thy [apply_def] "(lam x.b(x)) ` a = b(a)";
+goalw Term.thy [apply_def] "(lam x. b(x)) ` a = b(a)";
 by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam])));
 qed "applyB";
 
@@ -48,7 +48,7 @@
 qed "fixB";
 
 goalw Term.thy [letrec_def]
-      "letrec g x be h(x,g) in g(a) = h(a,%y.letrec g x be h(x,g) in g(y))";
+      "letrec g x be h(x,g) in g(a) = h(a,%y. letrec g x be h(x,g) in g(y))";
 by (resolve_tac [fixB RS ssubst] 1 THEN 
     resolve_tac [applyB RS ssubst] 1 THEN rtac refl 1);
 qed "letrecB";
@@ -98,10 +98,10 @@
 
 val letrec2B = raw_mk_beta_rl (data_defs @ [letrec2_def])
        "letrec g x y be h(x,y,g) in g(p,q) = \
-\                     h(p,q,%u v.letrec g x y be h(x,y,g) in g(u,v))";
+\                     h(p,q,%u v. letrec g x y be h(x,y,g) in g(u,v))";
 val letrec3B = raw_mk_beta_rl (data_defs @ [letrec3_def])
        "letrec g x y z be h(x,y,z,g) in g(p,q,r) = \
-\                     h(p,q,r,%u v w.letrec g x y z be h(x,y,z,g) in g(u,v,w))";
+\                     h(p,q,r,%u v w. letrec g x y z be h(x,y,z,g) in g(u,v,w))";
 
 val napplyBzero   = mk_beta_rl "f^zero`a = a";
 val napplyBsucc   = mk_beta_rl "f^succ(n)`a = f(f^n`a)";
diff -r f1a1817659e6 -r d7f033c74b38 src/CCL/Term.thy
--- a/src/CCL/Term.thy	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/Term.thy	Fri Oct 10 17:10:12 1997 +0200
@@ -54,36 +54,36 @@
 rules
 
   one_def                    "one == true"
-  if_def     "if b then t else u  == case(b,t,u,% x y.bot,%v.bot)"
+  if_def     "if b then t else u  == case(b,t,u,% x y. bot,%v. bot)"
   inl_def                 "inl(a) == <true,a>"
   inr_def                 "inr(b) == <false,b>"
-  when_def           "when(t,f,g) == split(t,%b x.if b then f(x) else g(x))"
-  split_def           "split(t,f) == case(t,bot,bot,f,%u.bot)"
-  fst_def                 "fst(t) == split(t,%x y.x)"
-  snd_def                 "snd(t) == split(t,%x y.y)"
-  thd_def                 "thd(t) == split(t,%x p.split(p,%y z.z))"
+  when_def           "when(t,f,g) == split(t,%b x. if b then f(x) else g(x))"
+  split_def           "split(t,f) == case(t,bot,bot,f,%u. bot)"
+  fst_def                 "fst(t) == split(t,%x y. x)"
+  snd_def                 "snd(t) == split(t,%x y. y)"
+  thd_def                 "thd(t) == split(t,%x p. split(p,%y z. z))"
   zero_def                  "zero == inl(one)"
   succ_def               "succ(n) == inr(n)"
-  ncase_def         "ncase(n,b,c) == when(n,%x.b,%y.c(y))"
-  nrec_def          " nrec(n,b,c) == letrec g x be ncase(x,b,%y.c(y,g(y))) in g(n)"
+  ncase_def         "ncase(n,b,c) == when(n,%x. b,%y. c(y))"
+  nrec_def          " nrec(n,b,c) == letrec g x be ncase(x,b,%y. c(y,g(y))) in g(n)"
   nil_def                     "[] == inl(one)"
   cons_def                   "h$t == inr(<h,t>)"
-  lcase_def         "lcase(l,b,c) == when(l,%x.b,%y.split(y,c))"
-  lrec_def           "lrec(l,b,c) == letrec g x be lcase(x,b,%h t.c(h,t,g(t))) in g(l)"
+  lcase_def         "lcase(l,b,c) == when(l,%x. b,%y. split(y,c))"
+  lrec_def           "lrec(l,b,c) == letrec g x be lcase(x,b,%h t. c(h,t,g(t))) in g(l)"
 
-  let_def  "let x be t in f(x) == case(t,f(true),f(false),%x y.f(<x,y>),%u.f(lam x.u(x)))"
+  let_def  "let x be t in f(x) == case(t,f(true),f(false),%x y. f(<x,y>),%u. f(lam x. u(x)))"
   letrec_def    
-  "letrec g x be h(x,g) in b(g) == b(%x.fix(%f.lam x.h(x,%y.f`y))`x)"
+  "letrec g x be h(x,g) in b(g) == b(%x. fix(%f. lam x. h(x,%y. f`y))`x)"
 
   letrec2_def  "letrec g x y be h(x,y,g) in f(g)== 
-               letrec g' p be split(p,%x y.h(x,y,%u v.g'(<u,v>))) 
-                          in f(%x y.g'(<x,y>))"
+               letrec g' p be split(p,%x y. h(x,y,%u v. g'(<u,v>))) 
+                          in f(%x y. g'(<x,y>))"
 
   letrec3_def  "letrec g x y z be h(x,y,z,g) in f(g) == 
-             letrec g' p be split(p,%x xs.split(xs,%y z.h(x,y,z,%u v w.g'(<u,<v,w>>)))) 
-                          in f(%x y z.g'(<x,<y,z>>))"
+             letrec g' p be split(p,%x xs. split(xs,%y z. h(x,y,z,%u v w. g'(<u,<v,w>>)))) 
+                          in f(%x y z. g'(<x,<y,z>>))"
 
-  napply_def "f ^n` a == nrec(n,a,%x g.f(g))"
+  napply_def "f ^n` a == nrec(n,a,%x g. f(g))"
 
 end
 
diff -r f1a1817659e6 -r d7f033c74b38 src/CCL/Type.ML
--- a/src/CCL/Type.ML	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/Type.ML	Fri Oct 10 17:10:12 1997 +0200
@@ -15,7 +15,7 @@
 val simp_data_defs = [one_def,inl_def,inr_def];
 val ind_data_defs = [zero_def,succ_def,nil_def,cons_def];
 
-goal Set.thy "A <= B <-> (ALL x.x:A --> x:B)";
+goal Set.thy "A <= B <-> (ALL x. x:A --> x:B)";
 by (fast_tac set_cs 1);
 qed "subsetXH";
 
@@ -25,18 +25,18 @@
 val XH_tac = mk_XH_tac Type.thy simp_type_defs [];
 
 val EmptyXH = XH_tac "a : {} <-> False";
-val SubtypeXH = XH_tac "a : {x:A.P(x)} <-> (a:A & P(a))";
+val SubtypeXH = XH_tac "a : {x:A. P(x)} <-> (a:A & P(a))";
 val UnitXH = XH_tac "a : Unit          <-> a=one";
 val BoolXH = XH_tac "a : Bool          <-> a=true | a=false";
-val PlusXH = XH_tac "a : A+B           <-> (EX x:A.a=inl(x)) | (EX x:B.a=inr(x))";
-val PiXH   = XH_tac "a : PROD x:A.B(x) <-> (EX b.a=lam x.b(x) & (ALL x:A.b(x):B(x)))";
-val SgXH   = XH_tac "a : SUM x:A.B(x)  <-> (EX x:A.EX y:B(x).a=<x,y>)";
+val PlusXH = XH_tac "a : A+B           <-> (EX x:A. a=inl(x)) | (EX x:B. a=inr(x))";
+val PiXH   = XH_tac "a : PROD x:A. B(x) <-> (EX b. a=lam x. b(x) & (ALL x:A. b(x):B(x)))";
+val SgXH   = XH_tac "a : SUM x:A. B(x)  <-> (EX x:A. EX y:B(x).a=<x,y>)";
 
 val XHs = [EmptyXH,SubtypeXH,UnitXH,BoolXH,PlusXH,PiXH,SgXH];
 
 val LiftXH = XH_tac "a : [A] <-> (a=bot | a:A)";
-val TallXH = XH_tac "a : TALL X.B(X) <-> (ALL X. a:B(X))";
-val TexXH  = XH_tac "a : TEX X.B(X) <-> (EX X. a:B(X))";
+val TallXH = XH_tac "a : TALL X. B(X) <-> (ALL X. a:B(X))";
+val TexXH  = XH_tac "a : TEX X. B(X) <-> (EX X. a:B(X))";
 
 val case_rls = XH_to_Es XHs;
 
@@ -49,7 +49,7 @@
 val oneT   = canT_tac "one : Unit";
 val trueT  = canT_tac "true : Bool";
 val falseT = canT_tac "false : Bool";
-val lamT   = canT_tac "[| !!x.x:A ==> b(x):B(x) |] ==> lam x.b(x) : Pi(A,B)";
+val lamT   = canT_tac "[| !!x. x:A ==> b(x):B(x) |] ==> lam x. b(x) : Pi(A,B)";
 val pairT  = canT_tac "[| a:A; b:B(a) |] ==> <a,b>:Sigma(A,B)";
 val inlT   = canT_tac "a:A ==> inl(a) : A+B";
 val inrT   = canT_tac "b:B ==> inr(b) : A+B";
@@ -108,16 +108,16 @@
 
 (*** Monotonicity ***)
 
-goal Type.thy "mono (%X.X)";
+goal Type.thy "mono (%X. X)";
 by (REPEAT (ares_tac [monoI] 1));
 qed "idM";
 
-goal Type.thy "mono(%X.A)";
+goal Type.thy "mono(%X. A)";
 by (REPEAT (ares_tac [monoI,subset_refl] 1));
 qed "constM";
 
 val major::prems = goal Type.thy
-    "mono(%X.A(X)) ==> mono(%X.[A(X)])";
+    "mono(%X. A(X)) ==> mono(%X.[A(X)])";
 by (rtac (subsetI RS monoI) 1);
 by (dtac (LiftXH RS iffD1) 1);
 by (etac disjE 1);
@@ -128,8 +128,8 @@
 qed "LiftM";
 
 val prems = goal Type.thy
-    "[| mono(%X.A(X)); !!x X. x:A(X) ==> mono(%X.B(X,x)) |] ==> \
-\    mono(%X.Sigma(A(X),B(X)))";
+    "[| mono(%X. A(X)); !!x X. x:A(X) ==> mono(%X. B(X,x)) |] ==> \
+\    mono(%X. Sigma(A(X),B(X)))";
 by (REPEAT (ares_tac ([subsetI RS monoI] @ canTs) 1 ORELSE
             eresolve_tac ([bspec,exE,conjE,disjE,bexE] @ case_rls) 1 ORELSE
             (resolve_tac (prems RL [monoD RS subsetD]) 1 THEN assume_tac 1) ORELSE
@@ -137,7 +137,7 @@
 qed "SgM";
 
 val prems = goal Type.thy
-    "[| !!x. x:A ==> mono(%X.B(X,x)) |] ==> mono(%X.Pi(A,B(X)))";
+    "[| !!x. x:A ==> mono(%X. B(X,x)) |] ==> mono(%X. Pi(A,B(X)))";
 by (REPEAT (ares_tac ([subsetI RS monoI] @ canTs) 1 ORELSE
             eresolve_tac ([bspec,exE,conjE,disjE,bexE] @ case_rls) 1 ORELSE
             (resolve_tac (prems RL [monoD RS subsetD]) 1 THEN assume_tac 1) ORELSE
@@ -145,7 +145,7 @@
 qed "PiM";
 
 val prems = goal Type.thy
-     "[| mono(%X.A(X));  mono(%X.B(X)) |] ==> mono(%X.A(X)+B(X))";
+     "[| mono(%X. A(X));  mono(%X. B(X)) |] ==> mono(%X. A(X)+B(X))";
 by (REPEAT (ares_tac ([subsetI RS monoI] @ canTs) 1 ORELSE
             eresolve_tac ([bspec,exE,conjE,disjE,bexE] @ case_rls) 1 ORELSE
             (resolve_tac (prems RL [monoD RS subsetD]) 1 THEN assume_tac 1) ORELSE
@@ -156,18 +156,18 @@
 
 (*** Conversion Rules for Fixed Points via monotonicity and Tarski ***)
 
-goal Type.thy "mono(%X.Unit+X)";
+goal Type.thy "mono(%X. Unit+X)";
 by (REPEAT (ares_tac [PlusM,constM,idM] 1));
 qed "NatM";
 bind_thm("def_NatB", result() RS (Nat_def RS def_lfp_Tarski));
 
-goal Type.thy "mono(%X.(Unit+Sigma(A,%y.X)))";
+goal Type.thy "mono(%X.(Unit+Sigma(A,%y. X)))";
 by (REPEAT (ares_tac [PlusM,SgM,constM,idM] 1));
 qed "ListM";
 bind_thm("def_ListB", result() RS (List_def RS def_lfp_Tarski));
 bind_thm("def_ListsB", result() RS (Lists_def RS def_gfp_Tarski));
 
-goal Type.thy "mono(%X.({} + Sigma(A,%y.X)))";
+goal Type.thy "mono(%X.({} + Sigma(A,%y. X)))";
 by (REPEAT (ares_tac [PlusM,SgM,constM,idM] 1));
 qed "IListsM";
 bind_thm("def_IListsB", result() RS (ILists_def RS def_gfp_Tarski));
@@ -182,10 +182,10 @@
 
 val iXH_tac = mk_iXH_tac ind_type_eqs ind_data_defs [];
 
-val NatXH  = iXH_tac "a : Nat <-> (a=zero | (EX x:Nat.a=succ(x)))";
-val ListXH = iXH_tac "a : List(A) <-> (a=[] | (EX x:A.EX xs:List(A).a=x$xs))";
-val ListsXH = iXH_tac "a : Lists(A) <-> (a=[] | (EX x:A.EX xs:Lists(A).a=x$xs))";
-val IListsXH = iXH_tac "a : ILists(A) <-> (EX x:A.EX xs:ILists(A).a=x$xs)";
+val NatXH  = iXH_tac "a : Nat <-> (a=zero | (EX x:Nat. a=succ(x)))";
+val ListXH = iXH_tac "a : List(A) <-> (a=[] | (EX x:A. EX xs:List(A).a=x$xs))";
+val ListsXH = iXH_tac "a : Lists(A) <-> (a=[] | (EX x:A. EX xs:Lists(A).a=x$xs))";
+val IListsXH = iXH_tac "a : ILists(A) <-> (EX x:A. EX xs:ILists(A).a=x$xs)";
 
 val iXHs = [NatXH,ListXH];
 val icase_rls = XH_to_Es iXHs;
@@ -283,15 +283,15 @@
 qed "lfp_subset_gfp";
 
 val prems = goal Type.thy
-    "[| a:A;  !!x X.[| x:A;  ALL y:A.t(y):X |] ==> t(x) : B(X) |] ==> \
+    "[| a:A;  !!x X.[| x:A;  ALL y:A. t(y):X |] ==> t(x) : B(X) |] ==> \
 \    t(a) : gfp(B)";
 by (rtac coinduct 1);
-by (res_inst_tac [("P","%x.EX y:A.x=t(y)")] CollectI 1);
+by (res_inst_tac [("P","%x. EX y:A. x=t(y)")] CollectI 1);
 by (ALLGOALS (fast_tac (ccl_cs addSIs prems)));
 qed "gfpI";
 
 val rew::prem::prems = goal Type.thy
-    "[| C==gfp(B);  a:A;  !!x X.[| x:A;  ALL y:A.t(y):X |] ==> t(x) : B(X) |] ==> \
+    "[| C==gfp(B);  a:A;  !!x X.[| x:A;  ALL y:A. t(y):X |] ==> t(x) : B(X) |] ==> \
 \    t(a) : C";
 by (rewtac rew);
 by (REPEAT (ares_tac ((prem RS gfpI)::prems) 1));
diff -r f1a1817659e6 -r d7f033c74b38 src/CCL/Type.thy
--- a/src/CCL/Type.thy	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/Type.thy	Fri Oct 10 17:10:12 1997 +0200
@@ -46,23 +46,23 @@
 
 rules
 
-  Subtype_def "{x:A.P(x)} == {x.x:A & P(x)}"
-  Unit_def          "Unit == {x.x=one}"
-  Bool_def          "Bool == {x.x=true | x=false}"
-  Plus_def           "A+B == {x. (EX a:A.x=inl(a)) | (EX b:B.x=inr(b))}"
-  Pi_def         "Pi(A,B) == {x.EX b.x=lam x.b(x) & (ALL x:A.b(x):B(x))}"
-  Sigma_def   "Sigma(A,B) == {x.EX a:A.EX b:B(a).x=<a,b>}"
-  Nat_def            "Nat == lfp(% X.Unit + X)"
-  List_def       "List(A) == lfp(% X.Unit + A*X)"
+  Subtype_def "{x:A. P(x)} == {x. x:A & P(x)}"
+  Unit_def          "Unit == {x. x=one}"
+  Bool_def          "Bool == {x. x=true | x=false}"
+  Plus_def           "A+B == {x. (EX a:A. x=inl(a)) | (EX b:B. x=inr(b))}"
+  Pi_def         "Pi(A,B) == {x. EX b. x=lam x. b(x) & (ALL x:A. b(x):B(x))}"
+  Sigma_def   "Sigma(A,B) == {x. EX a:A. EX b:B(a).x=<a,b>}"
+  Nat_def            "Nat == lfp(% X. Unit + X)"
+  List_def       "List(A) == lfp(% X. Unit + A*X)"
 
-  Lists_def     "Lists(A) == gfp(% X.Unit + A*X)"
+  Lists_def     "Lists(A) == gfp(% X. Unit + A*X)"
   ILists_def   "ILists(A) == gfp(% X.{} + A*X)"
 
-  Tall_def   "TALL X.B(X) == Inter({X.EX Y.X=B(Y)})"
-  Tex_def     "TEX X.B(X) == Union({X.EX Y.X=B(Y)})"
+  Tall_def   "TALL X. B(X) == Inter({X. EX Y. X=B(Y)})"
+  Tex_def     "TEX X. B(X) == Union({X. EX Y. X=B(Y)})"
   Lift_def           "[A] == A Un {bot}"
 
-  SPLIT_def   "SPLIT(p,B) == Union({A.EX x y.p=<x,y> & A=B(x,y)})"
+  SPLIT_def   "SPLIT(p,B) == Union({A. EX x y. p=<x,y> & A=B(x,y)})"
 
 end
 
diff -r f1a1817659e6 -r d7f033c74b38 src/CCL/Wfd.ML
--- a/src/CCL/Wfd.ML	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/Wfd.ML	Fri Oct 10 17:10:12 1997 +0200
@@ -25,7 +25,7 @@
 val [p1,p2,p3] = goal Wfd.thy
     "[| !!x y.<x,y> : R ==> Q(x); \
 \       ALL x. (ALL y. <y,x> : R --> y : P) --> x : P; \
-\       !!x.Q(x) ==> x:P |] ==> a:P";
+\       !!x. Q(x) ==> x:P |] ==> a:P";
 by (rtac (p2 RS  spec  RS mp) 1);
 by (fast_tac (set_cs addSIs [p1 RS p3]) 1);
 qed "wfd_strengthen_lemma";
@@ -64,7 +64,7 @@
 (*** Lexicographic Ordering ***)
 
 goalw Wfd.thy [lex_def] 
- "p : ra**rb <-> (EX a a' b b'.p = <<a,b>,<a',b'>> & (<a,a'> : ra | a=a' & <b,b'> : rb))";
+ "p : ra**rb <-> (EX a a' b b'. p = <<a,b>,<a',b'>> & (<a,a'> : ra | a=a' & <b,b'> : rb))";
 by (fast_tac ccl_cs 1);
 qed "lexXH";
 
@@ -98,7 +98,7 @@
  "[| Wfd(R); Wfd(S) |] ==> Wfd(R**S)";
 by (rewtac Wfd_def);
 by (safe_tac ccl_cs);
-by (wfd_strengthen_tac "%x.EX a b.x=<a,b>" 1);
+by (wfd_strengthen_tac "%x. EX a b. x=<a,b>" 1);
 by (fast_tac (term_cs addSEs [lex_pair]) 1);
 by (subgoal_tac "ALL a b.<a,b>:P" 1);
 by (fast_tac ccl_cs 1);
@@ -130,7 +130,7 @@
  "Wfd(r) ==> Wfd(wmap(f,r))";
 by (rewtac Wfd_def);
 by (safe_tac ccl_cs);
-by (subgoal_tac "ALL b.ALL a.f(a)=b-->a:P" 1);
+by (subgoal_tac "ALL b. ALL a. f(a)=b-->a:P" 1);
 by (fast_tac ccl_cs 1);
 by (rtac (wf RS wfd_induct RS allI) 1);
 by (safe_tac ccl_cs);
@@ -175,11 +175,11 @@
 by (rtac Empty_wf 1);
 qed "wf_wf";
 
-goalw Wfd.thy [NatPR_def]  "p : NatPR <-> (EX x:Nat.p=<x,succ(x)>)";
+goalw Wfd.thy [NatPR_def]  "p : NatPR <-> (EX x:Nat. p=<x,succ(x)>)";
 by (fast_tac set_cs 1);
 qed "NatPRXH";
 
-goalw Wfd.thy [ListPR_def]  "p : ListPR(A) <-> (EX h:A.EX t:List(A).p=<t,h$t>)";
+goalw Wfd.thy [ListPR_def]  "p : ListPR(A) <-> (EX h:A. EX t:List(A).p=<t,h$t>)";
 by (fast_tac set_cs 1);
 qed "ListPRXH";
 
@@ -188,7 +188,7 @@
 
 goalw Wfd.thy [Wfd_def]  "Wfd(NatPR)";
 by (safe_tac set_cs);
-by (wfd_strengthen_tac "%x.x:Nat" 1);
+by (wfd_strengthen_tac "%x. x:Nat" 1);
 by (fast_tac (type_cs addSEs [XH_to_E NatPRXH]) 1);
 by (etac Nat_ind 1);
 by (ALLGOALS (fast_tac (type_cs addEs [XH_to_E NatPRXH])));
@@ -196,7 +196,7 @@
 
 goalw Wfd.thy [Wfd_def]  "Wfd(ListPR(A))";
 by (safe_tac set_cs);
-by (wfd_strengthen_tac "%x.x:List(A)" 1);
+by (wfd_strengthen_tac "%x. x:List(A)" 1);
 by (fast_tac (type_cs addSEs [XH_to_E ListPRXH]) 1);
 by (etac List_ind 1);
 by (ALLGOALS (fast_tac (type_cs addEs [XH_to_E ListPRXH])));
diff -r f1a1817659e6 -r d7f033c74b38 src/CCL/Wfd.thy
--- a/src/CCL/Wfd.thy	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/Wfd.thy	Fri Oct 10 17:10:12 1997 +0200
@@ -21,14 +21,14 @@
 rules
 
   Wfd_def
-  "Wfd(R) == ALL P.(ALL x.(ALL y.<y,x> : R --> y:P) --> x:P) --> (ALL a.a:P)"
+  "Wfd(R) == ALL P.(ALL x.(ALL y.<y,x> : R --> y:P) --> x:P) --> (ALL a. a:P)"
 
-  wf_def         "wf(R) == {x.x:R & Wfd(R)}"
+  wf_def         "wf(R) == {x. x:R & Wfd(R)}"
 
   wmap_def       "wmap(f,R) == {p. EX x y. p=<x,y>  &  <f(x),f(y)> : R}"
   lex_def
-  "ra**rb == {p. EX a a' b b'.p = <<a,b>,<a',b'>> & (<a,a'> : ra | (a=a' & <b,b'> : rb))}"
+  "ra**rb == {p. EX a a' b b'. p = <<a,b>,<a',b'>> & (<a,a'> : ra | (a=a' & <b,b'> : rb))}"
 
-  NatPR_def      "NatPR == {p.EX x:Nat. p=<x,succ(x)>}"
-  ListPR_def     "ListPR(A) == {p.EX h:A.EX t:List(A). p=<t,h$t>}"
+  NatPR_def      "NatPR == {p. EX x:Nat. p=<x,succ(x)>}"
+  ListPR_def     "ListPR(A) == {p. EX h:A. EX t:List(A). p=<t,h$t>}"
 end
diff -r f1a1817659e6 -r d7f033c74b38 src/CCL/coinduction.ML
--- a/src/CCL/coinduction.ML	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/coinduction.ML	Fri Oct 10 17:10:12 1997 +0200
@@ -48,7 +48,7 @@
       ["<true,true> : POgen(R)",
        "<false,false> : POgen(R)",
        "[| <a,a'> : R;  <b,b'> : R |] ==> <<a,b>,<a',b'>> : POgen(R)",
-       "[|!!x. <b(x),b'(x)> : R |] ==><lam x.b(x),lam x.b'(x)> : POgen(R)",
+       "[|!!x. <b(x),b'(x)> : R |] ==><lam x. b(x),lam x. b'(x)> : POgen(R)",
        "<one,one> : POgen(R)",
        "<a,a'> : lfp(%x. POgen(x) Un R Un PO) ==> \
 \                         <inl(a),inl(a')> : POgen(lfp(%x. POgen(x) Un R Un PO))",
@@ -78,7 +78,7 @@
 ["<true,true> : EQgen(R)",
  "<false,false> : EQgen(R)",
  "[| <a,a'> : R;  <b,b'> : R |] ==> <<a,b>,<a',b'>> : EQgen(R)",
- "[|!!x. <b(x),b'(x)> : R |] ==> <lam x.b(x),lam x.b'(x)> : EQgen(R)",
+ "[|!!x. <b(x),b'(x)> : R |] ==> <lam x. b(x),lam x. b'(x)> : EQgen(R)",
  "<one,one> : EQgen(R)",
  "<a,a'> : lfp(%x. EQgen(x) Un R Un EQ) ==> \
 \                   <inl(a),inl(a')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))",
diff -r f1a1817659e6 -r d7f033c74b38 src/CCL/equalities.ML
--- a/src/CCL/equalities.ML	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/equalities.ML	Fri Oct 10 17:10:12 1997 +0200
@@ -64,11 +64,11 @@
 
 (** Simple properties of Compl -- complement of a set **)
 
-goal Set.thy "A Int Compl(A) = {x.False}";
+goal Set.thy "A Int Compl(A) = {x. False}";
 by (fast_tac eq_cs 1);
 qed "Compl_disjoint";
 
-goal Set.thy "A Un Compl(A) = {x.True}";
+goal Set.thy "A Un Compl(A) = {x. True}";
 by (fast_tac eq_cs 1);
 qed "Compl_partition";
 
@@ -106,7 +106,7 @@
 qed "Union_Un_distrib";
 
 val prems = goal Set.thy
-   "(Union(C) Int A = {x.False}) <-> (ALL B:C. B Int A = {x.False})";
+   "(Union(C) Int A = {x. False}) <-> (ALL B:C. B Int A = {x. False})";
 by (fast_tac (eq_cs addSEs [equalityE]) 1);
 qed "Union_disjoint";
 
diff -r f1a1817659e6 -r d7f033c74b38 src/CCL/eval.ML
--- a/src/CCL/eval.ML	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/eval.ML	Fri Oct 10 17:10:12 1997 +0200
@@ -14,7 +14,7 @@
 fun ceval_tac rls = DEPTH_SOLVE_1 (resolve_tac (!EVal_rls@rls) 1);
 
 val prems = goalw thy [apply_def]
-   "[| f ---> lam x.b(x);  b(a) ---> c |] ==> f ` a ---> c";
+   "[| f ---> lam x. b(x);  b(a) ---> c |] ==> f ` a ---> c";
 by (ceval_tac prems);
 qed "applyV";
 
@@ -35,7 +35,7 @@
 qed "fixV";
 
 val prems = goalw thy [letrec_def]
-    "h(t,%y.letrec g x be h(x,g) in g(y)) ---> c ==> \
+    "h(t,%y. letrec g x be h(x,g) in g(y)) ---> c ==> \
 \                  letrec g x be h(x,g) in g(t) ---> c";
 by (REPEAT (resolve_tac (prems @ [fixV,applyV,lamV]) 1));
 qed "letrecV";
@@ -69,19 +69,19 @@
 (* Factorial *)
 
 val prems = goal thy
-    "letrec f n be ncase(n,succ(zero),%x.nrec(n,zero,%y g.nrec(f(x),g,%z h.succ(h)))) \
+    "letrec f n be ncase(n,succ(zero),%x. nrec(n,zero,%y g. nrec(f(x),g,%z h. succ(h)))) \
 \              in f(succ(succ(zero))) ---> ?a";
 by (ceval_tac []);
 
 val prems = goal thy
-    "letrec f n be ncase(n,succ(zero),%x.nrec(n,zero,%y g.nrec(f(x),g,%z h.succ(h)))) \
+    "letrec f n be ncase(n,succ(zero),%x. nrec(n,zero,%y g. nrec(f(x),g,%z h. succ(h)))) \
 \              in f(succ(succ(succ(zero)))) ---> ?a";
 by (ceval_tac []);
 
 (* Less Than Or Equal *)
 
 fun isle x y = prove_goal thy 
-    ("letrec f p be split(p,%m n.ncase(m,true,%x.ncase(n,false,%y.f(<x,y>)))) \
+    ("letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f(<x,y>)))) \
 \              in f(<"^x^","^y^">) ---> ?a")
     (fn prems => [ceval_tac []]);
 
@@ -93,12 +93,12 @@
 (* Reverse *)
 
 val prems = goal thy
-    "letrec id l be lcase(l,[],%x xs.x$id(xs)) \
+    "letrec id l be lcase(l,[],%x xs. x$id(xs)) \
 \              in id(zero$succ(zero)$[]) ---> ?a";
 by (ceval_tac []);
 
 val prems = goal thy
-    "letrec rev l be lcase(l,[],%x xs.lrec(rev(xs),x$[],%y ys g.y$g)) \
-\              in rev(zero$succ(zero)$(succ((lam x.x)`succ(zero)))$([])) ---> ?a";
+    "letrec rev l be lcase(l,[],%x xs. lrec(rev(xs),x$[],%y ys g. y$g)) \
+\              in rev(zero$succ(zero)$(succ((lam x. x)`succ(zero)))$([])) ---> ?a";
 by (ceval_tac []);
 
diff -r f1a1817659e6 -r d7f033c74b38 src/CCL/ex/Flag.thy
--- a/src/CCL/ex/Flag.thy	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/ex/Flag.thy	Fri Oct 10 17:10:12 1997 +0200
@@ -24,11 +24,11 @@
   white_def    "white == inr(inl(one))"
   blue_def     "blue == inr(inr(one))"
 
-  ccase_def   "ccase(c,r,w,b) == when(c,%x.r,%wb.when(wb,%x.w,%x.b))"
+  ccase_def   "ccase(c,r,w,b) == when(c,%x. r,%wb. when(wb,%x. w,%x. b))"
 
-  flag_def    "flag == lam l.letrec 
+  flag_def    "flag == lam l. letrec 
       flagx l be lcase(l,<[],<[],[]>>, 
-                       %h t. split(flagx(t),%lr p.split(p,%lw lb. 
+                       %h t. split(flagx(t),%lr p. split(p,%lw lb. 
                             ccase(h, <red$lr,<lw,lb>>, 
                                      <lr,<white$lw,lb>>, 
                                      <lr,<lw,blue$lb>>)))) 
diff -r f1a1817659e6 -r d7f033c74b38 src/CCL/ex/List.ML
--- a/src/CCL/ex/List.ML	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/ex/List.ML	Fri Oct 10 17:10:12 1997 +0200
@@ -14,7 +14,7 @@
 (****)
 
 val listBs = map (fn s=>prove_goalw List.thy list_defs s (fn _ => [simp_tac term_ss 1]))
-     ["(f o g) = (%a.f(g(a)))",
+     ["(f o g) = (%a. f(g(a)))",
       "(f o g)(a) = f(g(a))",
       "map(f,[]) = []",
       "map(f,x$xs) = f(x)$map(f,xs)",
@@ -44,7 +44,7 @@
 (***)
 
 val prems = goalw List.thy [map_def]
-  "[| !!x.x:A==>f(x):B;  l : List(A) |] ==> map(f,l) : List(B)";
+  "[| !!x. x:A==>f(x):B;  l : List(A) |] ==> map(f,l) : List(B)";
 by (typechk_tac prems 1);
 qed "mapT";
 
diff -r f1a1817659e6 -r d7f033c74b38 src/CCL/ex/List.thy
--- a/src/CCL/ex/List.thy	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/ex/List.thy	Fri Oct 10 17:10:12 1997 +0200
@@ -22,15 +22,15 @@
 
 rules 
 
-  map_def     "map(f,l)   == lrec(l,[],%x xs g.f(x)$g)"
-  comp_def    "f o g == (%x.f(g(x)))"
-  append_def  "l @ m == lrec(l,m,%x xs g.x$g)"
-  mem_def     "a mem l == lrec(l,false,%h t g.if eq(a,h) then true else g)"
-  filter_def  "filter(f,l) == lrec(l,[],%x xs g.if f`x then x$g else g)"
-  flat_def    "flat(l) == lrec(l,[],%h t g.h @ g)"
+  map_def     "map(f,l)   == lrec(l,[],%x xs g. f(x)$g)"
+  comp_def    "f o g == (%x. f(g(x)))"
+  append_def  "l @ m == lrec(l,m,%x xs g. x$g)"
+  mem_def     "a mem l == lrec(l,false,%h t g. if eq(a,h) then true else g)"
+  filter_def  "filter(f,l) == lrec(l,[],%x xs g. if f`x then x$g else g)"
+  flat_def    "flat(l) == lrec(l,[],%h t g. h @ g)"
 
-  insert_def  "insert(f,a,l) == lrec(l,a$[],%h t g.if f`a`h then a$h$t else h$g)"
-  isort_def   "isort(f) == lam l.lrec(l,[],%h t g.insert(f,h,g))"
+  insert_def  "insert(f,a,l) == lrec(l,a$[],%h t g. if f`a`h then a$h$t else h$g)"
+  isort_def   "isort(f) == lam l. lrec(l,[],%h t g. insert(f,h,g))"
 
   partition_def 
   "partition(f,l) == letrec part l a b be lcase(l,<a,b>,%x xs.
@@ -38,7 +38,7 @@
                     in part(l,[],[])"
   qsort_def   "qsort(f) == lam l. letrec qsortx l be lcase(l,[],%h t. 
                                    let p be partition(f`h,t) 
-                                   in split(p,%x y.qsortx(x) @ h$qsortx(y))) 
+                                   in split(p,%x y. qsortx(x) @ h$qsortx(y))) 
                           in qsortx(l)"
 
 end
diff -r f1a1817659e6 -r d7f033c74b38 src/CCL/ex/Nat.thy
--- a/src/CCL/ex/Nat.thy	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/ex/Nat.thy	Fri Oct 10 17:10:12 1997 +0200
@@ -19,11 +19,11 @@
 
   not_def     "not(b) == if b then false else true"
 
-  add_def     "a #+ b == nrec(a,b,%x g.succ(g))"
-  mult_def    "a #* b == nrec(a,zero,%x g.b #+ g)"
-  sub_def     "a #- b == letrec sub x y be ncase(y,x,%yy.ncase(x,zero,%xx.sub(xx,yy))) 
+  add_def     "a #+ b == nrec(a,b,%x g. succ(g))"
+  mult_def    "a #* b == nrec(a,zero,%x g. b #+ g)"
+  sub_def     "a #- b == letrec sub x y be ncase(y,x,%yy. ncase(x,zero,%xx. sub(xx,yy))) 
                         in sub(a,b)"
-  le_def     "a #<= b == letrec le x y be ncase(x,true,%xx.ncase(y,false,%yy.le(xx,yy))) 
+  le_def     "a #<= b == letrec le x y be ncase(x,true,%xx. ncase(y,false,%yy. le(xx,yy))) 
                         in le(a,b)"
   lt_def     "a #< b == not(b #<= a)"
 
@@ -31,7 +31,7 @@
                        in div(a,b)"
   ack_def    
   "ackermann(a,b) == letrec ack n m be ncase(n,succ(m),%x. 
-                          ncase(m,ack(x,succ(zero)),%y.ack(x,ack(succ(x),y))))
+                          ncase(m,ack(x,succ(zero)),%y. ack(x,ack(succ(x),y))))
                     in ack(a,b)"
 
 end
diff -r f1a1817659e6 -r d7f033c74b38 src/CCL/ex/Stream.ML
--- a/src/CCL/ex/Stream.ML	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/ex/Stream.ML	Fri Oct 10 17:10:12 1997 +0200
@@ -16,7 +16,7 @@
 
 val prems = goal Stream.thy "l:Lists(A) ==> map(f o g,l) = map(f,map(g,l))";
 by (eq_coinduct3_tac 
-       "{p. EX x y.p=<x,y> & (EX l:Lists(A).x=map(f o g,l) & y=map(f,map(g,l)))}"  1);
+       "{p. EX x y. p=<x,y> & (EX l:Lists(A).x=map(f o g,l) & y=map(f,map(g,l)))}"  1);
 by (fast_tac (ccl_cs addSIs prems) 1);
 by (safe_tac type_cs);
 by (etac (XH_to_E ListsXH) 1);
@@ -27,9 +27,9 @@
 
 (*** Mapping the identity function leaves a list unchanged ***)
 
-val prems = goal Stream.thy "l:Lists(A) ==> map(%x.x,l) = l";
+val prems = goal Stream.thy "l:Lists(A) ==> map(%x. x,l) = l";
 by (eq_coinduct3_tac 
-       "{p. EX x y.p=<x,y> & (EX l:Lists(A).x=map(%x.x,l) & y=l)}"  1);
+       "{p. EX x y. p=<x,y> & (EX l:Lists(A).x=map(%x. x,l) & y=l)}"  1);
 by (fast_tac (ccl_cs addSIs prems) 1);
 by (safe_tac type_cs);
 by (etac (XH_to_E ListsXH) 1);
@@ -41,7 +41,7 @@
 
 val prems = goal Stream.thy 
         "[| l:Lists(A); m:Lists(A) |] ==> map(f,l@m) = map(f,l) @ map(f,m)";
-by (eq_coinduct3_tac "{p. EX x y.p=<x,y> & (EX l:Lists(A).EX m:Lists(A). \
+by (eq_coinduct3_tac "{p. EX x y. p=<x,y> & (EX l:Lists(A).EX m:Lists(A). \
 \                                           x=map(f,l@m) & y=map(f,l) @ map(f,m))}"  1);
 by (fast_tac (ccl_cs addSIs prems) 1);
 by (safe_tac type_cs);
@@ -57,7 +57,7 @@
 val prems = goal Stream.thy 
         "[| k:Lists(A); l:Lists(A); m:Lists(A) |] ==> k @ l @ m = (k @ l) @ m";
 by (eq_coinduct3_tac 
-    "{p. EX x y.p=<x,y> & (EX k:Lists(A).EX l:Lists(A).EX m:Lists(A). \
+    "{p. EX x y. p=<x,y> & (EX k:Lists(A).EX l:Lists(A).EX m:Lists(A). \
 \                          x=k @ l @ m & y=(k @ l) @ m)}"  1);
 by (fast_tac (ccl_cs addSIs prems) 1);
 by (safe_tac type_cs);
@@ -71,7 +71,7 @@
 
 val prems = goal Stream.thy "l:ILists(A) ==> l @ m = l";
 by (eq_coinduct3_tac
-    "{p. EX x y.p=<x,y> & (EX l:ILists(A).EX m.x=l@m & y=l)}" 1);
+    "{p. EX x y. p=<x,y> & (EX l:ILists(A).EX m. x=l@m & y=l)}" 1);
 by (fast_tac (ccl_cs addSIs prems) 1);
 by (safe_tac set_cs);
 by (etac (XH_to_E IListsXH) 1);
@@ -103,7 +103,7 @@
 
 goal Stream.thy "iter1(f,a) = iter2(f,a)";
 by (eq_coinduct3_tac 
-    "{p. EX x y.p=<x,y> & (EX n:Nat.x=iter1(f,f^n`a) & y=map(f)^n`iter2(f,a))}"
+    "{p. EX x y. p=<x,y> & (EX n:Nat. x=iter1(f,f^n`a) & y=map(f)^n`iter2(f,a))}"
     1);
 by (fast_tac (type_cs addSIs [napplyBzero RS sym,
                               napplyBzero RS sym RS arg_cong]) 1);
diff -r f1a1817659e6 -r d7f033c74b38 src/CCL/genrec.ML
--- a/src/CCL/genrec.ML	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/genrec.ML	Fri Oct 10 17:10:12 1997 +0200
@@ -30,7 +30,7 @@
 val prems = goalw Wfd.thy [letrec2_def]
     "[| a : A;  b : B;  \
 \     !!p q g.[| p:A; q:B; \
-\             ALL x:A.ALL y:{y: B. <<x,y>,<p,q>>:wf(R)}. g(x,y) : D(x,y) |] ==>\
+\             ALL x:A. ALL y:{y: B. <<x,y>,<p,q>>:wf(R)}. g(x,y) : D(x,y) |] ==>\
 \               h(p,q,g) : D(p,q) |] ==> \
 \    letrec g x y be h(x,y,g) in g(a,b) : D(a,b)";
 by (rtac (SPLITB RS subst) 1);
@@ -42,14 +42,14 @@
             eresolve_tac [bspec,SubtypeE,sym RS subst] 1));
 qed "letrec2T";
 
-goal Wfd.thy "SPLIT(<a,<b,c>>,%x xs.SPLIT(xs,%y z.B(x,y,z))) = B(a,b,c)";
+goal Wfd.thy "SPLIT(<a,<b,c>>,%x xs. SPLIT(xs,%y z. B(x,y,z))) = B(a,b,c)";
 by (simp_tac (ccl_ss addsimps [SPLITB]) 1);
 qed "lemma";
 
 val prems = goalw Wfd.thy [letrec3_def]
     "[| a : A;  b : B;  c : C;  \
 \    !!p q r g.[| p:A; q:B; r:C; \
-\      ALL x:A.ALL y:B.ALL z:{z:C. <<x,<y,z>>,<p,<q,r>>> : wf(R)}. \
+\      ALL x:A. ALL y:B. ALL z:{z:C. <<x,<y,z>>,<p,<q,r>>> : wf(R)}. \
 \                                                       g(x,y,z) : D(x,y,z) |] ==>\
 \               h(p,q,r,g) : D(p,q,r) |] ==> \
 \    letrec g x y z be h(x,y,z,g) in g(a,b,c) : D(a,b,c)";
@@ -75,14 +75,14 @@
 qed "rcallT";
 
 val major::prems = goal Wfd.thy
-    "[| ALL x:A.ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); \
+    "[| ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); \
 \       g(a,b) : D(a,b) ==> g(a,b) : E;  a:A;  b:B;  <<a,b>,<p,q>>:wf(R) |] ==> \
 \   g(a,b) : E";
 by (REPEAT (ares_tac ([SubtypeI,major RS bspec RS bspec,major]@prems) 1));
 qed "rcall2T";
 
 val major::prems = goal Wfd.thy
-    "[| ALL x:A.ALL y:B.ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}. g(x,y,z):D(x,y,z); \
+    "[| ALL x:A. ALL y:B. ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}. g(x,y,z):D(x,y,z); \
 \       g(a,b,c) : D(a,b,c) ==> g(a,b,c) : E;  \
 \       a:A;  b:B;  c:C;  <<a,<b,c>>,<p,<q,r>>> : wf(R) |] ==> \
 \   g(a,b,c) : E";
@@ -116,7 +116,7 @@
 qed "hyprcallT";
 
 val prems = goal Wfd.thy
-    "[| g(a,b) = c; ALL x:A.ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); \
+    "[| g(a,b) = c; ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); \
 \       [| c=g(a,b);  g(a,b) : D(a,b) |] ==> P; \
 \       a:A;  b:B;  <<a,b>,<p,q>>:wf(R) |] ==> \
 \   P";
@@ -128,7 +128,7 @@
 
 val prems = goal Wfd.thy
   "[| g(a,b,c) = d; \
-\     ALL x:A.ALL y:B.ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}.g(x,y,z):D(x,y,z); \
+\     ALL x:A. ALL y:B. ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}.g(x,y,z):D(x,y,z); \
 \   [| d=g(a,b,c);  g(a,b,c) : D(a,b,c) |] ==> P; \
 \   a:A;  b:B;  c:C;  <<a,<b,c>>,<p,<q,r>>> : wf(R) |] ==> \
 \   P";
@@ -149,13 +149,13 @@
 qed "rmIH1";
 
 val prems = goal Wfd.thy
-    "[| ALL x:A.ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); P |] ==> \
+    "[| ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); P |] ==> \
 \    P";
 by (REPEAT (ares_tac prems 1));
 qed "rmIH2";
 
 val prems = goal Wfd.thy
- "[| ALL x:A.ALL y:B.ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}.g(x,y,z):D(x,y,z); \
+ "[| ALL x:A. ALL y:B. ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}.g(x,y,z):D(x,y,z); \
 \    P |] ==> \
 \    P";
 by (REPEAT (ares_tac prems 1));
diff -r f1a1817659e6 -r d7f033c74b38 src/CCL/subset.ML
--- a/src/CCL/subset.ML	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/subset.ML	Fri Oct 10 17:10:12 1997 +0200
@@ -115,7 +115,7 @@
    "(a : Compl(B)) <->  (~a:B)",
    "(a : {b})      <->  (a=b)",
    "(a : {})       <->   False",
-   "(a : {x.P(x)}) <->  P(a)" ]);
+   "(a : {x. P(x)}) <->  P(a)" ]);
 
 val set_congs = [ball_cong, bex_cong, INT_cong, UN_cong];
 
diff -r f1a1817659e6 -r d7f033c74b38 src/CCL/typecheck.ML
--- a/src/CCL/typecheck.ML	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CCL/typecheck.ML	Fri Oct 10 17:10:12 1997 +0200
@@ -35,9 +35,9 @@
            fun solve s = prove_goal Type.thy s (fn prems => [tac prems])
        in map solve
            ["a : {x:A. b:{y:B(a).P(<x,y>)}} ==> <a,b> : {x:Sigma(A,B).P(x)}",
-            "a : {x:A.P(inl(x))} ==> inl(a) : {x:A+B.P(x)}",
-            "b : {x:B.P(inr(x))} ==> inr(b) : {x:A+B.P(x)}",
-            "a : {x:Nat.P(succ(x))} ==> succ(a) : {x:Nat.P(x)}",
+            "a : {x:A. P(inl(x))} ==> inl(a) : {x:A+B. P(x)}",
+            "b : {x:B. P(inr(x))} ==> inr(b) : {x:A+B. P(x)}",
+            "a : {x:Nat. P(succ(x))} ==> succ(a) : {x:Nat. P(x)}",
             "h : {x:A. t : {y:List(A).P(x$y)}} ==> h$t : {x:List(A).P(x)}"
         ] end;
 
@@ -54,12 +54,12 @@
 qed "applyT2";
 
 val prems = goal Type.thy 
-    "[| a:A;  a:A ==> P(a) |] ==> a : {x:A.P(x)}";
+    "[| a:A;  a:A ==> P(a) |] ==> a : {x:A. P(x)}";
 by (fast_tac (type_cs addSIs prems) 1);
 qed "rcall_lemma1";
 
 val prems = goal Type.thy 
-    "[| a:{x:A.Q(x)};  [| a:A; Q(a) |] ==> P(a) |] ==> a : {x:A.P(x)}";
+    "[| a:{x:A. Q(x)};  [| a:A; Q(a) |] ==> P(a) |] ==> a : {x:A. P(x)}";
 by (cut_facts_tac prems 1);
 by (fast_tac (type_cs addSIs prems) 1);
 qed "rcall_lemma2";
diff -r f1a1817659e6 -r d7f033c74b38 src/CTT/Arith.ML
--- a/src/CTT/Arith.ML	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CTT/Arith.ML	Fri Oct 10 17:10:12 1997 +0200
@@ -385,7 +385,7 @@
   [ (rew_tac(absdiff_typing::prems)) ]);
 
 qed_goalw "modC_succ" Arith.thy [mod_def] 
-"[| a:N; b:N |] ==> succ(a) mod b = rec(succ(a mod b) |-| b, 0, %x y.succ(a mod b)) : N"
+"[| a:N; b:N |] ==> succ(a) mod b = rec(succ(a mod b) |-| b, 0, %x y. succ(a mod b)) : N"
  (fn prems=>
   [ (rew_tac(absdiff_typing::prems)) ]);
 
@@ -429,7 +429,7 @@
 
 (*for case analysis on whether a number is 0 or a successor*)
 qed_goal "iszero_decidable" Arith.thy
-    "a:N ==> rec(a, inl(eq), %ka kb.inr(<ka, eq>)) : \
+    "a:N ==> rec(a, inl(eq), %ka kb. inr(<ka, eq>)) : \
 \                     Eq(N,a,0) + (SUM x:N. Eq(N,a, succ(x)))"
  (fn prems=>
   [ (NE_tac "a" 1),
diff -r f1a1817659e6 -r d7f033c74b38 src/CTT/Arith.thy
--- a/src/CTT/Arith.thy	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CTT/Arith.thy	Fri Oct 10 17:10:12 1997 +0200
@@ -15,10 +15,10 @@
        "#*",div,mod     :: "[i,i]=>i"   (infixr 70)
 
 rules
-  add_def     "a#+b == rec(a, b, %u v.succ(v))"  
-  diff_def    "a-b == rec(b, a, %u v.rec(v, 0, %x y.x))"  
+  add_def     "a#+b == rec(a, b, %u v. succ(v))"  
+  diff_def    "a-b == rec(b, a, %u v. rec(v, 0, %x y. x))"  
   absdiff_def "a|-|b == (a-b) #+ (b-a)"  
   mult_def    "a#*b == rec(a, 0, %u v. b #+ v)"  
-  mod_def     "a mod b == rec(a, 0, %u v. rec(succ(v) |-| b, 0, %x y.succ(v)))"
-  div_def     "a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y.v))"
+  mod_def     "a mod b == rec(a, 0, %u v. rec(succ(v) |-| b, 0, %x y. succ(v)))"
+  div_def     "a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y. v))"
 end
diff -r f1a1817659e6 -r d7f033c74b38 src/CTT/Bool.thy
--- a/src/CTT/Bool.thy	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CTT/Bool.thy	Fri Oct 10 17:10:12 1997 +0200
@@ -15,5 +15,5 @@
   Bool_def      "Bool == T+T"
   true_def      "true == inl(tt)"
   false_def     "false == inr(tt)"
-  cond_def      "cond(a,b,c) == when(a, %u.b, %u.c)"
+  cond_def      "cond(a,b,c) == when(a, %u. b, %u. c)"
 end
diff -r f1a1817659e6 -r d7f033c74b38 src/CTT/CTT.ML
--- a/src/CTT/CTT.ML	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CTT/CTT.ML	Fri Oct 10 17:10:12 1997 +0200
@@ -109,7 +109,7 @@
 
 (*Simplify the parameter of a unary type operator.*)
 qed_goal "subst_eqtyparg" CTT.thy
-    "a=c : A ==> (!!z.z:A ==> B(z) type) ==> B(a)=B(c)"
+    "a=c : A ==> (!!z. z:A ==> B(z) type) ==> B(a)=B(c)"
  (fn prems=>
   [ (rtac subst_typeL 1),
     (rtac refl_type 2),
diff -r f1a1817659e6 -r d7f033c74b38 src/CTT/CTT.thy
--- a/src/CTT/CTT.thy	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CTT/CTT.thy	Fri Oct 10 17:10:12 1997 +0200
@@ -113,21 +113,21 @@
 
   NE
    "[| p: N;  a: C(0);  !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |] 
-   ==> rec(p, a, %u v.b(u,v)) : C(p)"
+   ==> rec(p, a, %u v. b(u,v)) : C(p)"
 
   NEL
    "[| p = q : N;  a = c : C(0);  
       !!u v. [| u: N; v: C(u) |] ==> b(u,v) = d(u,v): C(succ(u)) |] 
-   ==> rec(p, a, %u v.b(u,v)) = rec(q,c,d) : C(p)"
+   ==> rec(p, a, %u v. b(u,v)) = rec(q,c,d) : C(p)"
 
   NC0
    "[| a: C(0);  !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |] 
-   ==> rec(0, a, %u v.b(u,v)) = a : C(0)"
+   ==> rec(0, a, %u v. b(u,v)) = a : C(0)"
 
   NC_succ
    "[| p: N;  a: C(0);  
        !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |] ==>  
-   rec(succ(p), a, %u v.b(u,v)) = b(p, rec(p, a, %u v.b(u,v))) : C(succ(p))"
+   rec(succ(p), a, %u v. b(u,v)) = b(p, rec(p, a, %u v. b(u,v))) : C(succ(p))"
 
   (*The fourth Peano axiom.  See page 91 of Martin-Lof's book*)
   zero_ne_succ
@@ -136,54 +136,54 @@
 
   (*The Product of a family of types*)
 
-  ProdF  "[| A type; !!x. x:A ==> B(x) type |] ==> PROD x:A.B(x) type"
+  ProdF  "[| A type; !!x. x:A ==> B(x) type |] ==> PROD x:A. B(x) type"
 
   ProdFL
    "[| A = C;  !!x. x:A ==> B(x) = D(x) |] ==> 
-   PROD x:A.B(x) = PROD x:C.D(x)"
+   PROD x:A. B(x) = PROD x:C. D(x)"
 
   ProdI
-   "[| A type;  !!x. x:A ==> b(x):B(x)|] ==> lam x.b(x) : PROD x:A.B(x)"
+   "[| A type;  !!x. x:A ==> b(x):B(x)|] ==> lam x. b(x) : PROD x:A. B(x)"
 
   ProdIL
    "[| A type;  !!x. x:A ==> b(x) = c(x) : B(x)|] ==> 
-   lam x.b(x) = lam x.c(x) : PROD x:A.B(x)"
+   lam x. b(x) = lam x. c(x) : PROD x:A. B(x)"
 
-  ProdE  "[| p : PROD x:A.B(x);  a : A |] ==> p`a : B(a)"
-  ProdEL "[| p=q: PROD x:A.B(x);  a=b : A |] ==> p`a = q`b : B(a)"
+  ProdE  "[| p : PROD x:A. B(x);  a : A |] ==> p`a : B(a)"
+  ProdEL "[| p=q: PROD x:A. B(x);  a=b : A |] ==> p`a = q`b : B(a)"
 
   ProdC
    "[| a : A;  !!x. x:A ==> b(x) : B(x)|] ==> 
-   (lam x.b(x)) ` a = b(a) : B(a)"
+   (lam x. b(x)) ` a = b(a) : B(a)"
 
   ProdC2
-   "p : PROD x:A.B(x) ==> (lam x. p`x) = p : PROD x:A.B(x)"
+   "p : PROD x:A. B(x) ==> (lam x. p`x) = p : PROD x:A. B(x)"
 
 
   (*The Sum of a family of types*)
 
-  SumF  "[| A type;  !!x. x:A ==> B(x) type |] ==> SUM x:A.B(x) type"
+  SumF  "[| A type;  !!x. x:A ==> B(x) type |] ==> SUM x:A. B(x) type"
   SumFL
-    "[| A = C;  !!x. x:A ==> B(x) = D(x) |] ==> SUM x:A.B(x) = SUM x:C.D(x)"
+    "[| A = C;  !!x. x:A ==> B(x) = D(x) |] ==> SUM x:A. B(x) = SUM x:C. D(x)"
 
-  SumI  "[| a : A;  b : B(a) |] ==> <a,b> : SUM x:A.B(x)"
-  SumIL "[| a=c:A;  b=d:B(a) |] ==> <a,b> = <c,d> : SUM x:A.B(x)"
+  SumI  "[| a : A;  b : B(a) |] ==> <a,b> : SUM x:A. B(x)"
+  SumIL "[| a=c:A;  b=d:B(a) |] ==> <a,b> = <c,d> : SUM x:A. B(x)"
 
   SumE
-    "[| p: SUM x:A.B(x);  !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>) |] 
-    ==> split(p, %x y.c(x,y)) : C(p)"
+    "[| p: SUM x:A. B(x);  !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>) |] 
+    ==> split(p, %x y. c(x,y)) : C(p)"
 
   SumEL
-    "[| p=q : SUM x:A.B(x); 
+    "[| p=q : SUM x:A. B(x); 
        !!x y. [| x:A; y:B(x) |] ==> c(x,y)=d(x,y): C(<x,y>)|] 
-    ==> split(p, %x y.c(x,y)) = split(q, % x y.d(x,y)) : C(p)"
+    ==> split(p, %x y. c(x,y)) = split(q, % x y. d(x,y)) : C(p)"
 
   SumC
     "[| a: A;  b: B(a);  !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>) |] 
-    ==> split(<a,b>, %x y.c(x,y)) = c(a,b) : C(<a,b>)"
+    ==> split(<a,b>, %x y. c(x,y)) = c(a,b) : C(<a,b>)"
 
-  fst_def   "fst(a) == split(a, %x y.x)"
-  snd_def   "snd(a) == split(a, %x y.y)"
+  fst_def   "fst(a) == split(a, %x y. x)"
+  snd_def   "snd(a) == split(a, %x y. y)"
 
 
   (*The sum of two types*)
@@ -200,22 +200,22 @@
   PlusE
     "[| p: A+B;  !!x. x:A ==> c(x): C(inl(x));  
                 !!y. y:B ==> d(y): C(inr(y)) |] 
-    ==> when(p, %x.c(x), %y.d(y)) : C(p)"
+    ==> when(p, %x. c(x), %y. d(y)) : C(p)"
 
   PlusEL
     "[| p = q : A+B;  !!x. x: A ==> c(x) = e(x) : C(inl(x));   
                      !!y. y: B ==> d(y) = f(y) : C(inr(y)) |] 
-    ==> when(p, %x.c(x), %y.d(y)) = when(q, %x.e(x), %y.f(y)) : C(p)"
+    ==> when(p, %x. c(x), %y. d(y)) = when(q, %x. e(x), %y. f(y)) : C(p)"
 
   PlusC_inl
     "[| a: A;  !!x. x:A ==> c(x): C(inl(x));  
               !!y. y:B ==> d(y): C(inr(y)) |] 
-    ==> when(inl(a), %x.c(x), %y.d(y)) = c(a) : C(inl(a))"
+    ==> when(inl(a), %x. c(x), %y. d(y)) = c(a) : C(inl(a))"
 
   PlusC_inr
     "[| b: B;  !!x. x:A ==> c(x): C(inl(x));  
               !!y. y:B ==> d(y): C(inr(y)) |] 
-    ==> when(inr(b), %x.c(x), %y.d(y)) = d(b) : C(inr(b))"
+    ==> when(inr(b), %x. c(x), %y. d(y)) = d(b) : C(inr(b))"
 
 
   (*The type Eq*)
diff -r f1a1817659e6 -r d7f033c74b38 src/CTT/ex/elim.ML
--- a/src/CTT/ex/elim.ML	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CTT/ex/elim.ML	Fri Oct 10 17:10:12 1997 +0200
@@ -148,7 +148,7 @@
 
 writeln"Axiom of choice.  Proof without fst, snd.  Harder still!"; 
 val prems = goal CTT.thy   
-    "[| A type;  !!x.x:A ==> B(x) type;                         \
+    "[| A type;  !!x. x:A ==> B(x) type;                         \
 \       !!x y.[| x:A;  y:B(x) |] ==> C(x,y) type                \
 \    |] ==> ?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).        \
 \                        (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
diff -r f1a1817659e6 -r d7f033c74b38 src/CTT/ex/equal.ML
--- a/src/CTT/ex/equal.ML	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CTT/ex/equal.ML	Fri Oct 10 17:10:12 1997 +0200
@@ -24,7 +24,7 @@
 
 (*in the "rec" formulation of addition, 0+n=n *)
 val prems =
-goal CTT.thy "p:N ==> rec(p,0, %y z.succ(y)) = p : N";
+goal CTT.thy "p:N ==> rec(p,0, %y z. succ(y)) = p : N";
 by (rtac EqE 1);
 by (resolve_tac elim_rls 1  THEN  resolve_tac prems 1);
 by (rew_tac prems);
@@ -33,7 +33,7 @@
 
 (*the harder version, n+0=n: recursive, uses induction hypothesis*)
 val prems =
-goal CTT.thy "p:N ==> rec(p,0, %y z.succ(z)) = p : N";
+goal CTT.thy "p:N ==> rec(p,0, %y z. succ(z)) = p : N";
 by (rtac EqE 1);
 by (resolve_tac elim_rls 1  THEN  resolve_tac prems 1);
 by (hyp_rew_tac prems);
@@ -43,8 +43,8 @@
 (*Associativity of addition*)
 val prems =
 goal CTT.thy
-   "[| a:N;  b:N;  c:N |] ==> rec(rec(a, b, %x y.succ(y)), c, %x y.succ(y)) = \
-\                   rec(a, rec(b, c, %x y.succ(y)), %x y.succ(y)) : N";
+   "[| a:N;  b:N;  c:N |] ==> rec(rec(a, b, %x y. succ(y)), c, %x y. succ(y)) = \
+\                   rec(a, rec(b, c, %x y. succ(y)), %x y. succ(y)) : N";
 by (NE_tac "a" 1);
 by (hyp_rew_tac prems);
 result();
@@ -53,7 +53,7 @@
 (*Martin-Lof (1984) page 62: pairing is surjective*)
 val prems =
 goal CTT.thy
-    "p : Sum(A,B) ==> <split(p,%x y.x), split(p,%x y.y)> = p : Sum(A,B)";
+    "p : Sum(A,B) ==> <split(p,%x y. x), split(p,%x y. y)> = p : Sum(A,B)";
 by (rtac EqE 1);
 by (resolve_tac elim_rls 1  THEN  resolve_tac prems 1);
 by (DEPTH_SOLVE_1 (rew_tac prems));   (*!!!!!!!*)
@@ -62,7 +62,7 @@
 
 val prems =
 goal CTT.thy "[| a : A;  b : B |] ==> \
-\    (lam u. split(u, %v w.<w,v>)) ` <a,b> = <b,a> : SUM x:B.A";
+\    (lam u. split(u, %v w.<w,v>)) ` <a,b> = <b,a> : SUM x:B. A";
 by (rew_tac prems);
 result();
 
@@ -71,7 +71,7 @@
 val prems =
 goal CTT.thy
    "(lam f. lam x. f`(f`x)) ` (lam u. split(u, %v w.<w,v>)) =  \
-\     lam x. x  :  PROD x:(SUM y:N.N). (SUM y:N.N)";
+\     lam x. x  :  PROD x:(SUM y:N. N). (SUM y:N. N)";
 by (resolve_tac reduction_rls 1);
 by (resolve_tac intrL_rls 3);
 by (rtac EqE 4);
diff -r f1a1817659e6 -r d7f033c74b38 src/CTT/ex/typechk.ML
--- a/src/CTT/ex/typechk.ML	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/CTT/ex/typechk.ML	Fri Oct 10 17:10:12 1997 +0200
@@ -45,17 +45,17 @@
 result(); 
 
 writeln"typechecking an application of fst";
-goal CTT.thy "(lam u. split(u, %v w.v)) ` <0, succ(0)> : ?A";
+goal CTT.thy "(lam u. split(u, %v w. v)) ` <0, succ(0)> : ?A";
 by (typechk_tac[]);
 result(); 
 
 writeln"typechecking the predecessor function";
-goal CTT.thy "lam n. rec(n, 0, %x y.x) : ?A";
+goal CTT.thy "lam n. rec(n, 0, %x y. x) : ?A";
 by (typechk_tac[]);
 result(); 
 
 writeln"typechecking the addition function";
-goal CTT.thy "lam n. lam m. rec(n, m, %x y.succ(y)) : ?A";
+goal CTT.thy "lam n. lam m. rec(n, m, %x y. succ(y)) : ?A";
 by (typechk_tac[]);
 result(); 
 
@@ -74,7 +74,7 @@
 result(); 
 
 writeln"typechecking fst (as a function object) ";
-goal CTT.thy "lam i. split(i, %j k.j) : ?A";
+goal CTT.thy "lam i. split(i, %j k. j) : ?A";
 by (typechk_tac[]);
 by N_tac;
 result(); 
diff -r f1a1817659e6 -r d7f033c74b38 src/LCF/LCF.ML
--- a/src/LCF/LCF.ML	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/LCF/LCF.ML	Fri Oct 10 17:10:12 1997 +0200
@@ -65,7 +65,7 @@
                       REPEAT(rstac(conjI::prems)1)]);
 
 val ext = prove_goal thy
-        "(!!x::'a::cpo. f(x)=(g(x)::'b::cpo)) ==> (%x.f(x))=(%x.g(x))"
+        "(!!x::'a::cpo. f(x)=(g(x)::'b::cpo)) ==> (%x. f(x))=(%x. g(x))"
         (fn [prem] => [REPEAT(rstac[less_anti_sym, less_ext, allI,
                                     prem RS eq_imp_less1,
                                     prem RS eq_imp_less2]1)]);
@@ -79,7 +79,7 @@
 val ap_term = refl RS cong;
 val ap_thm = refl RSN (2,cong);
 
-val UU_abs = prove_goal thy "(%x::'a::cpo.UU) = UU"
+val UU_abs = prove_goal thy "(%x::'a::cpo. UU) = UU"
         (fn _ => [rtac less_anti_sym 1, rtac minimal 2,
                   rtac less_ext 1, rtac allI 1, rtac minimal 1]);
 
@@ -89,7 +89,7 @@
         (fn prems=> [rtac less_anti_sym 1,rstac prems 1,rtac minimal 1]);
 
 
-val tr_induct = prove_goal thy "[| P(UU); P(TT); P(FF) |] ==> ALL b.P(b)"
+val tr_induct = prove_goal thy "[| P(UU); P(TT); P(FF) |] ==> ALL b. P(b)"
         (fn prems => [rtac allI 1, rtac mp 1,
                       res_inst_tac[("p","b")]tr_cases 2,
                       fast_tac (FOL_cs addIs prems) 1]);
diff -r f1a1817659e6 -r d7f033c74b38 src/LCF/LCF.thy
--- a/src/LCF/LCF.thy	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/LCF/LCF.thy	Fri Oct 10 17:10:12 1997 +0200
@@ -99,12 +99,12 @@
      Note that "easiness" of types is not taken into account
      because it cannot be expressed schematically; flatness could be. *)
 
-  adm_less      "adm(%x.t(x) << u(x))"
+  adm_less      "adm(%x. t(x) << u(x))"
   adm_not_less  "adm(%x.~ t(x) << u)"
-  adm_not_free  "adm(%x.A)"
-  adm_subst     "adm(P) ==> adm(%x.P(t(x)))"
-  adm_conj      "[| adm(P); adm(Q) |] ==> adm(%x.P(x)&Q(x))"
-  adm_disj      "[| adm(P); adm(Q) |] ==> adm(%x.P(x)|Q(x))"
-  adm_imp       "[| adm(%x.~P(x)); adm(Q) |] ==> adm(%x.P(x)-->Q(x))"
-  adm_all       "(!!y.adm(P(y))) ==> adm(%x.ALL y.P(y,x))"
+  adm_not_free  "adm(%x. A)"
+  adm_subst     "adm(P) ==> adm(%x. P(t(x)))"
+  adm_conj      "[| adm(P); adm(Q) |] ==> adm(%x. P(x)&Q(x))"
+  adm_disj      "[| adm(P); adm(Q) |] ==> adm(%x. P(x)|Q(x))"
+  adm_imp       "[| adm(%x.~P(x)); adm(Q) |] ==> adm(%x. P(x)-->Q(x))"
+  adm_all       "(!!y. adm(P(y))) ==> adm(%x. ALL y. P(y,x))"
 end
diff -r f1a1817659e6 -r d7f033c74b38 src/LCF/fix.ML
--- a/src/LCF/fix.ML	Fri Oct 10 16:29:41 1997 +0200
+++ b/src/LCF/fix.ML	Fri Oct 10 17:10:12 1997 +0200
@@ -22,7 +22,7 @@
 structure Fix:FIX =
 struct
 
-val adm_eq = prove_goal LCF.thy "adm(%x.t(x)=(u(x)::'a::cpo))"
+val adm_eq = prove_goal LCF.thy "adm(%x. t(x)=(u(x)::'a::cpo))"
         (fn _ => [rewtac eq_def,
                   REPEAT(rstac[adm_conj,adm_less]1)]);
 
@@ -41,7 +41,7 @@
 val not_eq_UU = prove_goal LCF.thy "ALL p. ~p=UU <-> (p=TT | p=FF)"
     (fn _ => [tac]) RS spec;
 
-val adm_not_eq_tr = prove_goal LCF.thy "ALL p::tr.adm(%x. ~t(x)=p)"
+val adm_not_eq_tr = prove_goal LCF.thy "ALL p::tr. adm(%x. ~t(x)=p)"
     (fn _ => [rtac tr_induct 1,
     REPEAT(simp_tac (LCF_ss addsimps [not_eq_TT,not_eq_FF,not_eq_UU]) 1 THEN
            REPEAT(rstac [adm_disj,adm_eq] 1))]) RS spec;
@@ -80,7 +80,7 @@
 val FIX2 = FIX_pair_conj RS conjunct2;
 
 val induct2 = prove_goal LCF.thy
-         "[| adm(%p.P(FST(p),SND(p))); P(UU::'a,UU::'b);\
+         "[| adm(%p. P(FST(p),SND(p))); P(UU::'a,UU::'b);\
 \            ALL x y. P(x,y) --> P(f(x),g(y)) |] ==> P(FIX(f),FIX(g))"
         (fn prems => [EVERY1
         [res_inst_tac [("f","f"),("g","g")] (standard(FIX1 RS ssubst)),