# HG changeset patch
# User wenzelm
# Date 876502948 -7200
# Node ID b55686a7b22c9b3a21fcc2003ccb509a1466cc66
# Parent  22bbc167676851be3efbe30193632e91671fd0c2
fixed dots;

diff -r 22bbc1676768 -r b55686a7b22c src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Arith.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -255,7 +255,7 @@
 
 (*non-strict, in 1st argument*)
 goal Arith.thy "!!i j k::nat. i<=j ==> i + k <= j + k";
-by (res_inst_tac [("f", "%j.j+k")] less_mono_imp_le_mono 1);
+by (res_inst_tac [("f", "%j. j+k")] less_mono_imp_le_mono 1);
 by (etac add_less_mono1 1);
 by (assume_tac 1);
 qed "add_le_mono1";
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Finite.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -215,8 +215,8 @@
 qed "finite_has_card";
 
 goal Finite.thy
-  "!!A.[| x ~: A; insert x A = {f i|i.i<n} |] ==> \
-\  ? m::nat. m<n & (? g. A = {g i|i.i<m})";
+  "!!A.[| x ~: A; insert x A = {f i|i. i<n} |] ==> \
+\  ? m::nat. m<n & (? g. A = {g i|i. i<m})";
 by (res_inst_tac [("n","n")] natE 1);
  by (hyp_subst_tac 1);
  by (Asm_full_simp_tac 1);
@@ -277,11 +277,11 @@
 val lemma = result();
 
 goal Finite.thy "!!A. [| finite A; x ~: A |] ==> \
-\ (LEAST n. ? f. insert x A = {f i|i.i<n}) = Suc(LEAST n. ? f. A={f i|i.i<n})";
+\ (LEAST n. ? f. insert x A = {f i|i. i<n}) = Suc(LEAST n. ? f. A={f i|i. i<n})";
 by (rtac Least_equality 1);
  by (dtac finite_has_card 1);
  by (etac exE 1);
- by (dres_inst_tac [("P","%n.? f. A={f i|i.i<n}")] LeastI 1);
+ by (dres_inst_tac [("P","%n.? f. A={f i|i. i<n}")] LeastI 1);
  by (etac exE 1);
  by (res_inst_tac
    [("x","%i. if i<(LEAST n. ? f. A={f i |i. i < n}) then f i else x")] exI 1);
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Fun.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -46,7 +46,7 @@
 by (etac arg_cong 1);
 qed "inj_eq";
 
-val [major] = goal Fun.thy "inj(f) ==> (@x.f(x)=f(y)) = y";
+val [major] = goal Fun.thy "inj(f) ==> (@x. f(x)=f(y)) = y";
 by (rtac (major RS injD) 1);
 by (rtac selectI 1);
 by (rtac refl 1);
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/Gfp.ML
--- a/src/HOL/Gfp.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Gfp.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -73,13 +73,13 @@
          - instead of the condition  X <= f(X)
                            consider  X <= (f(X) Un f(f(X)) ...) Un gfp(X) ***)
 
-val [prem] = goal Gfp.thy "mono(f) ==> mono(%x.f(x) Un X Un B)";
+val [prem] = goal Gfp.thy "mono(f) ==> mono(%x. f(x) Un X 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
-    "[| X <= f(lfp(%x.f(x) Un X Un gfp(f)));  mono(f) |] ==> \
-\    lfp(%x.f(x) Un X Un gfp(f)) <= f(lfp(%x.f(x) Un X Un gfp(f)))";
+    "[| X <= f(lfp(%x. f(x) Un X Un gfp(f)));  mono(f) |] ==> \
+\    lfp(%x. f(x) Un X Un gfp(f)) <= f(lfp(%x. f(x) Un X 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);
@@ -92,7 +92,7 @@
 qed "coinduct3_lemma";
 
 val prems = goal Gfp.thy
-    "[| mono(f);  a:X;  X <= f(lfp(%x.f(x) Un X Un gfp(f))) |] ==> a : gfp(f)";
+    "[| mono(f);  a:X;  X <= f(lfp(%x. f(x) Un X Un gfp(f))) |] ==> a : gfp(f)";
 by (rtac (coinduct3_lemma RSN (2,weak_coinduct)) 1);
 by (resolve_tac (prems RL [coinduct3_mono_lemma RS lfp_Tarski RS ssubst]) 1);
 by (rtac (UnI2 RS UnI1) 1);
@@ -123,7 +123,7 @@
 qed "def_Collect_coinduct";
 
 val rew::prems = goal Gfp.thy
-    "[| A==gfp(f); mono(f);  a:X;  X <= f(lfp(%x.f(x) Un X Un A)) |] ==> a: A";
+    "[| A==gfp(f); mono(f);  a:X;  X <= f(lfp(%x. f(x) Un X Un A)) |] ==> a: A";
 by (rewtac rew);
 by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems @ [coinduct3]) 1));
 qed "def_coinduct3";
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/HOL.ML
--- a/src/HOL/HOL.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/HOL.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -90,15 +90,15 @@
 qed_goalw "allI" HOL.thy [All_def] "(!!x::'a. P(x)) ==> !x. P(x)"
  (fn prems => [resolve_tac (prems RL [eqTrueI RS ext]) 1]);
 
-qed_goalw "spec" HOL.thy [All_def] "! x::'a.P(x) ==> P(x)"
+qed_goalw "spec" HOL.thy [All_def] "! x::'a. P(x) ==> P(x)"
  (fn prems => [rtac eqTrueE 1, resolve_tac (prems RL [fun_cong]) 1]);
 
-qed_goal "allE" HOL.thy "[| !x.P(x);  P(x) ==> R |] ==> R"
+qed_goal "allE" HOL.thy "[| !x. P(x);  P(x) ==> R |] ==> R"
  (fn major::prems=>
   [ (REPEAT (resolve_tac (prems @ [major RS spec]) 1)) ]);
 
 qed_goal "all_dupE" HOL.thy 
-    "[| ! x.P(x);  [| P(x); ! x.P(x) |] ==> R |] ==> R"
+    "[| ! x. P(x);  [| P(x); ! x. P(x) |] ==> R |] ==> R"
  (fn prems =>
   [ (REPEAT (resolve_tac (prems @ (prems RL [spec])) 1)) ]);
 
@@ -155,11 +155,11 @@
 (** Existential quantifier **)
 section "?";
 
-qed_goalw "exI" HOL.thy [Ex_def] "P(x) ==> ? x::'a.P(x)"
+qed_goalw "exI" HOL.thy [Ex_def] "P(x) ==> ? x::'a. P(x)"
  (fn prems => [rtac selectI 1, resolve_tac prems 1]);
 
 qed_goalw "exE" HOL.thy [Ex_def]
-  "[| ? x::'a.P(x); !!x. P(x) ==> Q |] ==> Q"
+  "[| ? x::'a. P(x); !!x. P(x) ==> Q |] ==> Q"
   (fn prems => [REPEAT(resolve_tac prems 1)]);
 
 
@@ -237,12 +237,12 @@
 
 (*Sometimes easier to use: the premises have no shared variables.  Safe!*)
 qed_goal "ex_ex1I" HOL.thy
-    "[| ? x.P(x);  !!x y. [| P(x); P(y) |] ==> x=y |] ==> ?! x. P(x)"
+    "[| ? x. P(x);  !!x y. [| P(x); P(y) |] ==> x=y |] ==> ?! x. P(x)"
  (fn [ex,eq] => [ (rtac (ex RS exE) 1),
                   (REPEAT (ares_tac [ex1I,eq] 1)) ]);
 
 qed_goalw "ex1E" HOL.thy [Ex1_def]
-    "[| ?! x.P(x);  !!x. [| P(x);  ! y. P(y) --> y=x |] ==> R |] ==> R"
+    "[| ?! x. P(x);  !!x. [| P(x);  ! y. P(y) --> y=x |] ==> R |] ==> R"
  (fn major::prems =>
   [rtac (major RS exE) 1, REPEAT (etac conjE 1 ORELSE ares_tac prems 1)]);
 
@@ -252,23 +252,23 @@
 
 (*Easier to apply than selectI: conclusion has only one occurrence of P*)
 qed_goal "selectI2" HOL.thy
-    "[| P(a);  !!x. P(x) ==> Q(x) |] ==> Q(@x.P(x))"
+    "[| P(a);  !!x. P(x) ==> Q(x) |] ==> Q(@x. P(x))"
  (fn prems => [ resolve_tac prems 1, 
                 rtac selectI 1, 
                 resolve_tac prems 1 ]);
 
 (*Easier to apply than selectI2 if witness ?a comes from an EX-formula*)
 qed_goal "selectI2EX" HOL.thy
-  "[| ? a.P a; !!x. P x ==> Q x |] ==> Q(Eps P)"
+  "[| ? a. P a; !!x. P x ==> Q x |] ==> Q(Eps P)"
 (fn [major,minor] => [rtac (major RS exE) 1, etac selectI2 1, etac minor 1]);
 
 qed_goal "select_equality" HOL.thy
-    "[| P(a);  !!x. P(x) ==> x=a |] ==> (@x.P(x)) = a"
+    "[| P(a);  !!x. P(x) ==> x=a |] ==> (@x. P(x)) = a"
  (fn prems => [ rtac selectI2 1, 
                 REPEAT (ares_tac prems 1) ]);
 
 qed_goalw "select1_equality" HOL.thy [Ex1_def]
-  "!!P. [| ?!x.P(x); P(a) |] ==> (@x.P(x)) = a"
+  "!!P. [| ?!x. P(x); P(a) |] ==> (@x. P(x)) = a"
 (fn _ => [rtac select_equality 1, atac 1,
           etac exE 1, etac conjE 1,
           rtac allE 1, atac 1,
@@ -313,7 +313,7 @@
     (REPEAT (DEPTH_SOLVE_1 
         (eresolve_tac ([asm_rl,impCE,notE]@prems) 1))) ]);
 
-qed_goal "exCI" HOL.thy "(! x. ~P(x) ==> P(a)) ==> ? x.P(x)"
+qed_goal "exCI" HOL.thy "(! x. ~P(x) ==> P(a)) ==> ? x. P(x)"
  (fn prems=>
   [ (rtac ccontr 1),
     (REPEAT (ares_tac (prems@[exI,allI,notI,notE]) 1))  ]);
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/HOL.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -106,7 +106,7 @@
 
 translations
   "x ~= y"      == "~ (x = y)"
-  "@ x.b"       == "Eps (%x. b)"
+  "@ x. b"      == "Eps (%x. b)"
   "ALL xs. P"   => "! xs. P"
   "EX xs. P"    => "? xs. P"
   "EX! xs. P"   => "?! xs. P"
@@ -149,18 +149,18 @@
 
   refl          "t = (t::'a)"
   subst         "[| s = t; P(s) |] ==> P(t::'a)"
-  ext           "(!!x::'a. (f(x)::'b) = g(x)) ==> (%x.f(x)) = (%x.g(x))"
-  selectI       "P(x::'a) ==> P(@x.P(x))"
+  ext           "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)"
+  selectI       "P (x::'a) ==> P (@x. P x)"
 
   impI          "(P ==> Q) ==> P-->Q"
   mp            "[| P-->Q;  P |] ==> Q"
 
 defs
 
-  True_def      "True      == ((%x::bool.x)=(%x.x))"
-  All_def       "All(P)    == (P = (%x.True))"
-  Ex_def        "Ex(P)     == P(@x.P(x))"
-  False_def     "False     == (!P.P)"
+  True_def      "True      == ((%x::bool. x) = (%x. x))"
+  All_def       "All(P)    == (P = (%x. True))"
+  Ex_def        "Ex(P)     == P(@x. P(x))"
+  False_def     "False     == (!P. P)"
   not_def       "~ P       == P-->False"
   and_def       "P & Q     == !R. (P-->Q-->R) --> R"
   or_def        "P | Q     == !R. (P-->R) --> (Q-->R) --> R"
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/Hoare/Arith2.ML
--- a/src/HOL/Hoare/Arith2.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Hoare/Arith2.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -62,7 +62,7 @@
 
 val prems=goalw thy [gcd_def] "n<=m ==> gcd m n = gcd (m-n) n";
 by (cut_facts_tac prems 1);
-by (subgoal_tac "n<=m ==> !x.cd x m n = cd x (m-n) n" 1);
+by (subgoal_tac "n<=m ==> !x. cd x m n = cd x (m-n) n" 1);
 by (Asm_simp_tac 1);
 by (rtac allI 1);
 by (etac cd_diff_l 1);
@@ -70,7 +70,7 @@
 
 val prems=goalw thy [gcd_def] "m<=n ==> gcd m n = gcd m (n-m)";
 by (cut_facts_tac prems 1);
-by (subgoal_tac "m<=n ==> !x.cd x m n = cd x m (n-m)" 1);
+by (subgoal_tac "m<=n ==> !x. cd x m n = cd x m (n-m)" 1);
 by (Asm_simp_tac 1);
 by (rtac allI 1);
 by (etac cd_diff_r 1);
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/Hoare/Arith2.thy
--- a/src/HOL/Hoare/Arith2.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Hoare/Arith2.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -16,7 +16,7 @@
   "gcd m n     == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
 
   pow     :: [nat, nat] => nat                              (infixl 75)
-  "m pow n     == nat_rec (Suc 0) (%u v.m*v) n"
+  "m pow n     == nat_rec (Suc 0) (%u v. m*v) n"
 
   fac     :: nat => nat
   "fac m       == nat_rec (Suc 0) (%u v.(Suc u)*v) m"
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/Hoare/Hoare.ML
--- a/src/HOL/Hoare/Hoare.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Hoare/Hoare.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -11,20 +11,20 @@
 (*** Hoare rules ***)
 
 val SkipRule = prove_goalw thy [Spec_def,Skip_def]
-  "(!!s.p(s) ==> q(s)) ==> Spec p Skip q"
+  "(!!s. p(s) ==> q(s)) ==> Spec p Skip q"
   (fn prems => [fast_tac (!claset addIs prems) 1]);
 
 val AssignRule = prove_goalw thy [Spec_def,Assign_def]
-  "(!!s. p s ==> q(%x.if x=v then e s else s x)) ==> Spec p (Assign v e) q"
+  "(!!s. p s ==> q(%x. if x=v then e s else s x)) ==> Spec p (Assign v e) q"
   (fn prems => [fast_tac (!claset addIs prems) 1]);
 
 val SeqRule = prove_goalw thy [Spec_def,Seq_def]
-  "[| Spec p c (%s.q s); Spec (%s.q s) c' r |] ==> Spec p (Seq c c') r"
+  "[| Spec p c (%s. q s); Spec (%s. q s) c' r |] ==> Spec p (Seq c c') r"
   (fn prems => [cut_facts_tac prems 1, Fast_tac 1]);
 
 val IfRule = prove_goalw thy [Spec_def,Cond_def]
   "[| !!s. p s ==> (b s --> q s) & (~b s --> q' s); \
-\     Spec (%s.q s) c r; Spec (%s.q' s) c' r |] \
+\     Spec (%s. q s) c r; Spec (%s. q' s) c' r |] \
 \  ==> Spec p (Cond b c c') r"
   (fn [prem1,prem2,prem3] =>
      [REPEAT (rtac allI 1),
@@ -39,7 +39,7 @@
                        fast_tac (!claset addIs [prem1]) 1]);
 
 val lemma = prove_goalw thy [Spec_def,While_def]
-  "[| Spec (%s.I s & b s) c I; !!s. [| I s; ~b s |] ==> q s |] \
+  "[| Spec (%s. I s & b s) c I; !!s. [| I s; ~b s |] ==> q s |] \
 \  ==> Spec I (While b I c) q"
   (fn [prem1,prem2] =>
      [REPEAT(rtac allI 1), rtac impI 1, etac exE 1, rtac mp 1, atac 2,
@@ -134,7 +134,7 @@
 (* VarsElimTac: Taktik zum Eliminieren von bestimmten Programmvariablen aus dem Subgoal i
  - v::vl:(term) list  Liste der zu eliminierenden Programmvariablen
  - meta_spec:thm      Theorem, welches zur Entfernung der Variablen benutzt wird
-		      z.B.: "(!!s x.PROP P(s,x)) ==> (!!s.PROP P(s,x(s)))"
+		      z.B.: "(!!s x. PROP P(s,x)) ==> (!!s. PROP P(s,x(s)))"
  - namexAll:string    Name von    ^                                  (hier "x")
  - varx:term          Term zu                                      ^ (hier Var(("x",0),...))
  - varP:term          Term zu                                  ^     (hier Var(("P",0),...))
@@ -144,25 +144,25 @@
       - eliminiere jede pvar durch Anwendung von comp_inst_ren_tac. Dazu:
       - Unbenennung in meta_spec: namexAll wird in den Namen der Prog.-Var. umbenannt
 	z.B.: fuer die Prog.-Var. mit Namen "a" ergibt sich
-	      meta_spec zu "(!! s a.PROP P(s,a)) ==> (!! s.PROP P(s,x(s)))"
+	      meta_spec zu "(!! s a. PROP P(s,a)) ==> (!! s. PROP P(s,x(s)))"
       - Instanziierungen in meta_spec:
-	      varx wird mit "%s:(type_pvar) state.s(pvar)" instanziiert
+	      varx wird mit "%s:(type_pvar) state. s(pvar)" instanziiert
 	      varP wird entsprechend instanziiert. Beispiel fuer Prog.-Var. "a":
-	 - zu Subgoal "!!s.s(Suc(0)) = s(0) ==> s(0) = 1" bestimme Term ohne "!!s.":
+	 - zu Subgoal "!!s. s(Suc(0)) = s(0) ==> s(0) = 1" bestimme Term ohne "!!s.":
 		trm0 = "s(Suc(0)) = s(0) ==> s(0) = 1" (s ist hier freie Variable)
 	 - substituiere alle Vorkommen von s(pvar) durch eine freie Var. xs:
 		trm1 = "s(Suc(0)) = xs ==> xs = 1"
 	 - abstrahiere ueber xs:
-		trm2 = "%xs.s(Suc(0)) = xs ==> xs = 1"
+		trm2 = "%xs. s(Suc(0)) = xs ==> xs = 1"
 	 - abstrahiere ueber restliche Vorkommen von s:
-		trm3 = "%s xs.s(Suc(0)) = xs ==> xs = 1"
+		trm3 = "%s xs. s(Suc(0)) = xs ==> xs = 1"
 	 - instanziiere varP mit trm3
 *)
 
 (* StateElimTac: tactic to eliminate all program variable from subgoal i
-    - applies to subgoals of the form "!!s:('a) state.P(s)",
+    - applies to subgoals of the form "!!s:('a) state. P(s)",
         i.e. the term  Const("all",_) $ Abs ("s",pvar --> 'a,_)
-    -   meta_spec has the form "(!!s x.PROP P(s,x)) ==> (!!s.PROP P(s,x(s)))"
+    -   meta_spec has the form "(!!s x. PROP P(s,x)) ==> (!!s. PROP P(s,x(s)))"
 *)
 
 val StateElimTac = SUBGOAL (fn (Bi,i) =>
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/Hoare/Hoare.thy
--- a/src/HOL/Hoare/Hoare.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Hoare/Hoare.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -34,7 +34,7 @@
   "Skip s s' == (s=s')"
 
   Assign        :: [pvar, 'a exp] => 'a com
-  "Assign v e s s' == (s' = (%x.if x=v then e(s) else s(x)))"
+  "Assign v e s s' == (s' = (%x. if x=v then e(s) else s(x)))"
 
   Seq           :: ['a com, 'a com] => 'a com
   "Seq c c' s s' == ? s''. c s s'' & c' s'' s'"
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/IMP/Hoare.ML
--- a/src/HOL/IMP/Hoare.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/IMP/Hoare.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -27,7 +27,7 @@
 by (Simp_tac 1);
 qed "wp_SKIP";
 
-goalw Hoare.thy [wp_def] "wp (x:=a) Q = (%s.Q(s[a s/x]))";
+goalw Hoare.thy [wp_def] "wp (x:=a) Q = (%s. Q(s[a s/x]))";
 by (Simp_tac 1);
 qed "wp_Ass";
 
@@ -66,7 +66,7 @@
 
 goal thy
   "wp (WHILE b DO c) Q s = \
-\  (s : gfp(%S.{s.if b s then wp c (%s.s:S) s else Q s}))";
+\  (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))";
 by (simp_tac (!simpset setloop(split_tac[expand_if])) 1);
 by (rtac iffI 1);
  by (rtac weak_coinduct 1);
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/IMP/Hoare.thy
--- a/src/HOL/IMP/Hoare.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/IMP/Hoare.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -20,7 +20,7 @@
 inductive hoare
 intrs
   skip "|- {P}SKIP{P}"
-  ass  "|- {%s.P(s[a s/x])} x:=a {P}"
+  ass  "|- {%s. P(s[a s/x])} x:=a {P}"
   semi "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}"
   If "[| |- {%s. P s & b s}c{Q}; |- {%s. P s & ~b s}d{Q} |] ==>
       |- {P} IF b THEN c ELSE d {Q}"
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/IMP/VC.ML
--- a/src/HOL/IMP/VC.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/IMP/VC.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -10,7 +10,7 @@
 
 AddIs hoare.intrs;
 
-val lemma = prove_goal HOL.thy "!s.P s --> P s" (K[Fast_tac 1]);
+val lemma = prove_goal HOL.thy "!s. P s --> P s" (K[Fast_tac 1]);
 
 goal VC.thy "!Q. (!s. vc c Q s) --> |- {awp c Q} astrip c {Q}";
 by (acom.induct_tac "c" 1);
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/IMP/VC.thy
--- a/src/HOL/IMP/VC.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/IMP/VC.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -23,14 +23,14 @@
 
 primrec awp acom
   "awp Askip Q = Q"
-  "awp (Aass x a) Q = (%s.Q(s[a s/x]))"
+  "awp (Aass x a) Q = (%s. Q(s[a s/x]))"
   "awp (Asemi c d) Q = awp c (awp d Q)"
   "awp (Aif b c d) Q = (%s. (b s-->awp c Q s) & (~b s-->awp d Q s))" 
   "awp (Awhile b I c) Q = I"
 
 primrec vc acom
-  "vc Askip Q = (%s.True)"
-  "vc (Aass x a) Q = (%s.True)"
+  "vc Askip Q = (%s. True)"
+  "vc (Aass x a) Q = (%s. True)"
   "vc (Asemi c d) Q = (%s. vc c (awp d Q) s & vc d Q s)"
   "vc (Aif b c d) Q = (%s. vc c Q s & vc d Q s)" 
   "vc (Awhile b I c) Q = (%s. (I s & ~b s --> Q s) &
@@ -45,8 +45,8 @@
 
 (* simultaneous computation of vc and awp: *)
 primrec vcawp acom
-  "vcawp Askip Q = (%s.True, Q)"
-  "vcawp (Aass x a) Q = (%s.True, %s.Q(s[a s/x]))"
+  "vcawp Askip Q = (%s. True, Q)"
+  "vcawp (Aass x a) Q = (%s. True, %s. Q(s[a s/x]))"
   "vcawp (Asemi c d) Q = (let (vcd,wpd) = vcawp d Q;
                               (vcc,wpc) = vcawp c wpd
                           in (%s. vcc s & vcd s, wpc))"
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/IOA/IOA.ML
--- a/src/HOL/IOA/IOA.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/IOA/IOA.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -47,7 +47,7 @@
 qed "mk_trace_thm";
 
 goalw IOA.thy [reachable_def] "!!A. s:starts_of(A) ==> reachable A s";
-  by (res_inst_tac [("x","(%i.None,%i.s)")] bexI 1);
+  by (res_inst_tac [("x","(%i. None,%i. s)")] bexI 1);
   by (Simp_tac 1);
   by (asm_simp_tac (!simpset addsimps exec_rws) 1);
 qed "reachable_0";
@@ -56,9 +56,9 @@
 "!!A. [| reachable A s; (s,a,t) : trans_of(A) |] ==> reachable A t";
   by (asm_full_simp_tac (!simpset delsimps bex_simps) 1);
   by (safe_tac (!claset));
-  by (res_inst_tac [("x","(%i.if i<n then fst ex i                    \
+  by (res_inst_tac [("x","(%i. if i<n then fst ex i                    \
 \                            else (if i=n then Some a else None),    \
-\                         %i.if i<Suc n then snd ex i else t)")] bexI 1);
+\                         %i. if i<Suc n then snd ex i else t)")] bexI 1);
   by (res_inst_tac [("x","Suc(n)")] exI 1);
   by (Simp_tac 1);
   by (Asm_simp_tac 1);
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/IOA/IOA.thy
--- a/src/HOL/IOA/IOA.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/IOA/IOA.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -104,13 +104,13 @@
 (* Restrict the trace to those members of the set s *)
 filter_oseq_def
   "filter_oseq p s ==                                                   
-   (%i.case s(i)                                                       
+   (%i. case s(i)                                                       
          of None => None                                               
           | Some(x) => if p x then Some x else None)"
 
 
 mk_trace_def
-  "mk_trace(ioa) == filter_oseq(%a.a:externals(asig_of(ioa)))"
+  "mk_trace(ioa) == filter_oseq(%a. a:externals(asig_of(ioa)))"
 
 
 (* Does an ioa have an execution with the given trace *)
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/IOA/Solve.ML
--- a/src/HOL/IOA/Solve.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/IOA/Solve.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -22,7 +22,7 @@
   by (Asm_full_simp_tac 1);
 
   (* give execution of abstract automata *)
-  by (res_inst_tac[("x","(mk_trace A (fst ex),%i.f(snd ex i))")] bexI 1);
+  by (res_inst_tac[("x","(mk_trace A (fst ex),%i. f(snd ex i))")] bexI 1);
 
   (* Traces coincide *)
   by (asm_simp_tac (!simpset addsimps [mk_trace_def,filter_oseq_idemp])1);
@@ -68,9 +68,9 @@
 by (asm_full_simp_tac (!simpset addsimps [reachable_def]) 1); 
 by (etac bexE 1);
 by (res_inst_tac [("x",
-   "(filter_oseq (%a.a:actions(asig_of(C1))) \
+   "(filter_oseq (%a. a:actions(asig_of(C1))) \
 \                (fst ex),                                                \
-\    %i.fst (snd ex i))")]  bexI 1);
+\    %i. fst (snd ex i))")]  bexI 1);
 (* fst(s) is in projected execution *)
  by (Simp_tac 1);
  by (Fast_tac 1);
@@ -88,9 +88,9 @@
 by (asm_full_simp_tac (!simpset addsimps [reachable_def]) 1); 
 by (etac bexE 1);
 by (res_inst_tac [("x",
-   "(filter_oseq (%a.a:actions(asig_of(C2)))\
+   "(filter_oseq (%a. a:actions(asig_of(C2)))\
 \                (fst ex),                                                \
-\    %i.snd (snd ex i))")]  bexI 1);
+\    %i. snd (snd ex i))")]  bexI 1);
 (* fst(s) is in projected execution *)
  by (Simp_tac 1);
  by (Fast_tac 1);
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/Induct/LFilter.ML
--- a/src/HOL/Induct/LFilter.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Induct/LFilter.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -178,7 +178,7 @@
 
 (*** lfilter: simple facts by coinduction ***)
 
-goal thy "lfilter (%x.True) l = l";
+goal thy "lfilter (%x. True) l = l";
 by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
 by (ALLGOALS Simp_tac);
 by (Blast_tac 1);
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/Induct/LList.ML
--- a/src/HOL/Induct/LList.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Induct/LList.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -62,16 +62,16 @@
 (*** LList_corec satisfies the desired recurion equation ***)
 
 (*A continuity result?*)
-goalw LList.thy [CONS_def] "CONS M (UN x.f(x)) = (UN x. CONS M (f x))";
+goalw LList.thy [CONS_def] "CONS M (UN x. f(x)) = (UN x. CONS M (f x))";
 by (simp_tac (!simpset addsimps [In1_UN1, Scons_UN1_y]) 1);
 qed "CONS_UN1";
 
 (*UNUSED; obsolete?
-goal Prod.thy "split p (%x y.UN z.f x y z) = (UN z. split p (%x y.f x y z))";
+goal Prod.thy "split p (%x y. UN z. f x y z) = (UN z. split p (%x y. f x y z))";
 by (simp_tac (!simpset setloop (split_tac [expand_split])) 1);
 qed "split_UN1";
 
-goal Sum.thy "sum_case s f (%y.UN z.g y z) = (UN z.sum_case s f (%y.g y z))";
+goal Sum.thy "sum_case s f (%y. UN z. g y z) = (UN z. sum_case s f (%y. g y z))";
 by (simp_tac (!simpset setloop (split_tac [expand_sum_case])) 1);
 qed "sum_case2_UN1";
 *)
@@ -87,7 +87,7 @@
 (** The directions of the equality are proved separately **)
 
 goalw LList.thy [LList_corec_def]
-    "LList_corec a f <= sum_case (%u.NIL) \
+    "LList_corec a f <= sum_case (%u. NIL) \
 \                          (split(%z w. CONS z (LList_corec w f))) (f a)";
 by (rtac UN1_least 1);
 by (res_inst_tac [("n","k")] natE 1);
@@ -96,7 +96,7 @@
 qed "LList_corec_subset1";
 
 goalw LList.thy [LList_corec_def]
-    "sum_case (%u.NIL) (split(%z w. CONS z (LList_corec w f))) (f a) <= \
+    "sum_case (%u. NIL) (split(%z w. CONS z (LList_corec w f))) (f a) <= \
 \    LList_corec a f";
 by (simp_tac (!simpset addsimps [CONS_UN1]) 1);
 by (safe_tac (!claset));
@@ -114,15 +114,15 @@
 (*definitional version of same*)
 val [rew] = goal LList.thy
     "[| !!x. h(x) == LList_corec x f |] ==>     \
-\    h(a) = sum_case (%u.NIL) (split(%z w. CONS z (h w))) (f a)";
+\    h(a) = sum_case (%u. NIL) (split(%z w. CONS z (h w))) (f a)";
 by (rewtac rew);
 by (rtac LList_corec 1);
 qed "def_LList_corec";
 
 (*A typical use of co-induction to show membership in the gfp. 
   Bisimulation is  range(%x. LList_corec x f) *)
-goal LList.thy "LList_corec a f : llist({u.True})";
-by (res_inst_tac [("X", "range(%x.LList_corec x ?g)")] llist_coinduct 1);
+goal LList.thy "LList_corec a f : llist({u. True})";
+by (res_inst_tac [("X", "range(%x. LList_corec x ?g)")] llist_coinduct 1);
 by (rtac rangeI 1);
 by (safe_tac (!claset));
 by (stac LList_corec 1);
@@ -132,9 +132,9 @@
 
 (*Lemma for the proof of llist_corec*)
 goal LList.thy
-   "LList_corec a (%z.sum_case Inl (split(%v w.Inr((Leaf(v),w)))) (f z)) : \
+   "LList_corec a (%z. sum_case Inl (split(%v w. Inr((Leaf(v),w)))) (f z)) : \
 \   llist(range Leaf)";
-by (res_inst_tac [("X", "range(%x.LList_corec x ?g)")] llist_coinduct 1);
+by (res_inst_tac [("X", "range(%x. LList_corec x ?g)")] llist_coinduct 1);
 by (rtac rangeI 1);
 by (safe_tac (!claset));
 by (stac LList_corec 1);
@@ -263,12 +263,12 @@
 
 (*abstract proof using a bisimulation*)
 val [prem1,prem2] = goal LList.thy
- "[| !!x. h1(x) = sum_case (%u.NIL) (split(%z w. CONS z (h1 w))) (f x);  \
-\    !!x. h2(x) = sum_case (%u.NIL) (split(%z w. CONS z (h2 w))) (f x) |]\
+ "[| !!x. h1(x) = sum_case (%u. NIL) (split(%z w. CONS z (h1 w))) (f x);  \
+\    !!x. h2(x) = sum_case (%u. NIL) (split(%z w. CONS z (h2 w))) (f x) |]\
 \ ==> h1=h2";
 by (rtac ext 1);
 (*next step avoids an unknown (and flexflex pair) in simplification*)
-by (res_inst_tac [("A", "{u.True}"),
+by (res_inst_tac [("A", "{u. True}"),
                   ("r", "range(%u. (h1(u),h2(u)))")] LList_equalityI 1);
 by (rtac rangeI 1);
 by (safe_tac (!claset));
@@ -280,8 +280,8 @@
 qed "LList_corec_unique";
 
 val [prem] = goal LList.thy
- "[| !!x. h(x) = sum_case (%u.NIL) (split(%z w. CONS z (h w))) (f x) |] \
-\ ==> h = (%x.LList_corec x f)";
+ "[| !!x. h(x) = sum_case (%u. NIL) (split(%z w. CONS z (h w))) (f x) |] \
+\ ==> h = (%x. LList_corec x f)";
 by (rtac (LList_corec RS (prem RS LList_corec_unique)) 1);
 qed "equals_LList_corec";
 
@@ -298,8 +298,8 @@
 qed "ntrunc_CONS";
 
 val [prem1,prem2] = goal LList.thy
- "[| !!x. h1(x) = sum_case (%u.NIL) (split(%z w. CONS z (h1 w))) (f x);  \
-\    !!x. h2(x) = sum_case (%u.NIL) (split(%z w. CONS z (h2 w))) (f x) |]\
+ "[| !!x. h1(x) = sum_case (%u. NIL) (split(%z w. CONS z (h1 w))) (f x);  \
+\    !!x. h2(x) = sum_case (%u. NIL) (split(%z w. CONS z (h2 w))) (f x) |]\
 \ ==> h1=h2";
 by (rtac (ntrunc_equality RS ext) 1);
 by (rename_tac "x k" 1);
@@ -338,14 +338,14 @@
 by (REPEAT (ares_tac [list_Fun_CONS_I, singletonI, UnI1] 1));
 qed "Lconst_type";
 
-goal LList.thy "Lconst(M) = LList_corec M (%x.Inr((x,x)))";
+goal LList.thy "Lconst(M) = LList_corec M (%x. Inr((x,x)))";
 by (rtac (equals_LList_corec RS fun_cong) 1);
 by (Simp_tac 1);
 by (rtac Lconst 1);
 qed "Lconst_eq_LList_corec";
 
 (*Thus we could have used gfp in the definition of Lconst*)
-goal LList.thy "gfp(%N. CONS M N) = LList_corec M (%x.Inr((x,x)))";
+goal LList.thy "gfp(%N. CONS M N) = LList_corec M (%x. Inr((x,x)))";
 by (rtac (equals_LList_corec RS fun_cong) 1);
 by (Simp_tac 1);
 by (rtac (Lconst_fun_mono RS gfp_Tarski) 1);
@@ -485,7 +485,7 @@
                       rangeI RS LListD_Fun_CONS_I] 1));
 qed "Lmap_compose";
 
-val [prem] = goal LList.thy "M: llist(A) ==> Lmap (%x.x) M = M";
+val [prem] = goal LList.thy "M: llist(A) ==> Lmap (%x. x) M = M";
 by (rtac (prem RS imageI RS LList_equalityI) 1);
 by (safe_tac (!claset));
 by (etac llist.elim 1);
@@ -547,7 +547,7 @@
 (*strong co-induction: bisimulation and case analysis on one variable*)
 goal LList.thy
     "!!M N. [| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
-by (res_inst_tac [("X", "(%u.Lappend u N)``llist(A)")] llist_coinduct 1);
+by (res_inst_tac [("X", "(%u. Lappend u N)``llist(A)")] llist_coinduct 1);
 by (etac imageI 1);
 by (rtac subsetI 1);
 by (etac imageE 1);
@@ -605,7 +605,7 @@
 (*definitional version of same*)
 val [rew] = goal LList.thy
     "[| !!x. h(x) == llist_corec x f |] ==>     \
-\    h(a) = sum_case (%u.LNil) (split(%z w. LCons z (h w))) (f a)";
+\    h(a) = sum_case (%u. LNil) (split(%z w. LCons z (h w))) (f a)";
 by (rewtac rew);
 by (rtac llist_corec 1);
 qed "def_llist_corec";
@@ -740,7 +740,7 @@
 by (ALLGOALS Simp_tac);
 qed "lmap_compose";
 
-goal LList.thy "lmap (%x.x) l = l";
+goal LList.thy "lmap (%x. x) l = l";
 by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
 by (ALLGOALS Simp_tac);
 qed "lmap_ident";
@@ -793,8 +793,8 @@
     "(!!x. h(x) = LCons x (lmap f (h x))) ==> h = iterates(f)";
 by (rtac ext 1);
 by (res_inst_tac [("r", 
-   "UN u. range(%n. (nat_rec (h u) (%m y.lmap f y) n, \
-\                    nat_rec (iterates f u) (%m y.lmap f y) n))")] 
+   "UN u. range(%n. (nat_rec (h u) (%m y. lmap f y) n, \
+\                    nat_rec (iterates f u) (%m y. lmap f y) n))")] 
     llist_equalityI 1);
 by (REPEAT (resolve_tac [UN1_I, range_eqI, Pair_cong, nat_rec_0 RS sym] 1));
 by (safe_tac (!claset));
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/Induct/LList.thy
--- a/src/HOL/Induct/LList.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Induct/LList.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -11,7 +11,7 @@
 bounds on the amount of lookahead required.
 
 Could try (but would it work for the gfp analogue of term?)
-  LListD_Fun_def "LListD_Fun(A) == (%Z.diag({Numb(0)}) <++> diag(A) <**> Z)"
+  LListD_Fun_def "LListD_Fun(A) == (%Z. diag({Numb(0)}) <++> diag(A) <**> Z)"
 
 A nice but complex example would be [ML for the Working Programmer, page 176]
   from(1) = enumerate (Lmap (Lmap(pack), makeqq(from(1),from(1))))
@@ -74,7 +74,7 @@
             |] ==> (CONS a M, CONS b N) : LListD(r)"
 
 translations
-  "case p of LNil => a | LCons x l => b" == "llist_case a (%x l.b) p"
+  "case p of LNil => a | LCons x l => b" == "llist_case a (%x l. b) p"
 
 
 defs
@@ -108,7 +108,7 @@
   llist_corec_def
    "llist_corec a f == 
        Abs_llist(LList_corec a 
-                 (%z.case f z of Inl x    => Inl(x)
+                 (%z. case f z of Inl x    => Inl(x)
                                | Inr(v,w) => Inr(Leaf(v), w)))"
 
   llistD_Fun_def
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/Induct/PropLog.thy
--- a/src/HOL/Induct/PropLog.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Induct/PropLog.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -33,14 +33,14 @@
   eval_def "tt[p] == eval2 p tt"
 
 primrec eval2 pl
-  "eval2(false) = (%x.False)"
-  "eval2(#v) = (%tt.v:tt)"
-  "eval2(p->q) = (%tt.eval2 p tt-->eval2 q tt)"
+  "eval2(false) = (%x. False)"
+  "eval2(#v) = (%tt. v:tt)"
+  "eval2(p->q) = (%tt. eval2 p tt-->eval2 q tt)"
 
 primrec hyps pl
   "hyps(false) = (%tt.{})"
   "hyps(#v) = (%tt.{if v:tt then #v else #v->false})"
-  "hyps(p->q) = (%tt.hyps p tt Un hyps q tt)"
+  "hyps(p->q) = (%tt. hyps p tt Un hyps q tt)"
 
 end
 
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/Induct/SList.ML
--- a/src/HOL/Induct/SList.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Induct/SList.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -315,7 +315,7 @@
 by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
 qed "mem_append2";
 
-goal SList.thy "x mem [x:xs.P(x)] = (x mem xs & P(x))";
+goal SList.thy "x mem [x:xs. P(x)] = (x mem xs & P(x))";
 by (list_ind_tac "xs" 1);
 by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
 qed "mem_filter2";
@@ -347,7 +347,7 @@
 
 (** Additional mapping lemmas **)
 
-goal SList.thy "map (%x.x) xs = xs";
+goal SList.thy "map (%x. x) xs = xs";
 by (list_ind_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "map_ident2";
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/Induct/SList.thy
--- a/src/HOL/Induct/SList.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Induct/SList.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -56,9 +56,9 @@
   "[x]"         == "x#[]"
   "[]"          == "Nil"
 
-  "case xs of Nil => a | y#ys => b" == "list_case a (%y ys.b) xs"
+  "case xs of Nil => a | y#ys => b" == "list_case a (%y ys. b) xs"
 
-  "[x:xs . P]"  == "filter (%x.P) xs"
+  "[x:xs . P]"  == "filter (%x. P) xs"
 
 defs
   (* Defining the Concrete Constructors *)
@@ -82,7 +82,7 @@
   Nil_def       "Nil == Abs_list(NIL)"
   Cons_def      "x#xs == Abs_list(CONS (Leaf x) (Rep_list xs))"
 
-  List_case_def "List_case c d == Case (%x.c) (Split d)"
+  List_case_def "List_case c d == Case (%x. c) (Split d)"
 
   (* list Recursion -- the trancl is Essential; see list.ML *)
 
@@ -99,11 +99,11 @@
   Rep_map_def "Rep_map f xs == list_rec xs NIL (%x l r. CONS (f x) r)"
   Abs_map_def "Abs_map g M == List_rec M Nil (%N L r. g(N)#r)"
 
-  null_def      "null(xs)            == list_rec xs True (%x xs r.False)"
-  hd_def        "hd(xs)              == list_rec xs arbitrary (%x xs r.x)"
-  tl_def        "tl(xs)              == list_rec xs arbitrary (%x xs r.xs)"
+  null_def      "null(xs)            == list_rec xs True (%x xs r. False)"
+  hd_def        "hd(xs)              == list_rec xs arbitrary (%x xs r. x)"
+  tl_def        "tl(xs)              == list_rec xs arbitrary (%x xs r. xs)"
   (* a total version of tl: *)
-  ttl_def       "ttl(xs)             == list_rec xs [] (%x xs r.xs)"
+  ttl_def       "ttl(xs)             == list_rec xs [] (%x xs r. xs)"
 
   set_def       "set xs              == list_rec xs {} (%x l r. insert x r)"
 
@@ -114,6 +114,6 @@
   filter_def    "filter P xs         == 
                   list_rec xs [] (%x xs r. if P(x) then x#r else r)"
 
-  list_case_def  "list_case a f xs == list_rec xs a (%x xs r.f x xs)"
+  list_case_def  "list_case a f xs == list_rec xs a (%x xs r. f x xs)"
 
 end
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/Induct/Simult.ML
--- a/src/HOL/Induct/Simult.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Induct/Simult.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -87,8 +87,8 @@
 \       Q(Fnil);        \
 \       !!t ts. [| P(t);  Q(ts) |] ==> Q(Fcons t ts)    \
 \    |] ==> (! t. P(t)) & (! ts. Q(ts))";
-by (res_inst_tac [("P1","%z.P(Abs_Tree(z))"),
-                  ("Q1","%z.Q(Abs_Forest(z))")] 
+by (res_inst_tac [("P1","%z. P(Abs_Tree(z))"),
+                  ("Q1","%z. Q(Abs_Forest(z))")] 
     (Tree_Forest_induct RS conjE) 1);
 (*Instantiates ?A1 to range(Leaf). *)
 by (fast_tac (!claset addSEs [Rep_Tree_inverse RS subst, 
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/Induct/Term.ML
--- a/src/HOL/Induct/Term.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Induct/Term.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -37,7 +37,7 @@
 (*Induction for the set term(A) *)
 val [major,minor] = goal Term.thy 
     "[| M: term(A);  \
-\       !!x zs. [| x: A;  zs: list(term(A));  zs: list({x.R(x)}) \
+\       !!x zs. [| x: A;  zs: list(term(A));  zs: list({x. R(x)}) \
 \               |] ==> R(x$zs)  \
 \    |] ==> R(M)";
 by (rtac (major RS term.induct) 1);
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/Lex/AutoChopper.ML
--- a/src/HOL/Lex/AutoChopper.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Lex/AutoChopper.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -42,7 +42,7 @@
 bind_thm("no_acc", result() RS spec RS spec RS mp);
 
 
-val [prem] = goal HOL.thy "? x.P(f(x)) ==> ? y.P(y)";
+val [prem] = goal HOL.thy "? x. P(f(x)) ==> ? y. P(y)";
 by (cut_facts_tac [prem] 1);
 by (Fast_tac 1);
 val ex_special = result();
@@ -108,9 +108,9 @@
  by (Asm_simp_tac 1);
  by (case_tac "acc_prefix A (next A st a) list" 1);
   by (strip_tac 1);
-  by (res_inst_tac [("f","%k.a#k")] ex_special 1);
+  by (res_inst_tac [("f","%k. a#k")] ex_special 1);
   by (Simp_tac 1);
-  by (res_inst_tac [("t","%k.ys=r@a#k"),("s","%k.ys=(r@[a])@k")] subst 1);
+  by (res_inst_tac [("t","%k. ys=r@a#k"),("s","%k. ys=(r@[a])@k")] subst 1);
    by (Simp_tac 1);
   by (Fast_tac 1);
  by (strip_tac 1);
@@ -121,9 +121,9 @@
   by (Fast_tac 1);
  by (Simp_tac 1);
 by (strip_tac 1);
-by (res_inst_tac [("f","%k.a#k")] ex_special 1);
+by (res_inst_tac [("f","%k. a#k")] ex_special 1);
 by (Simp_tac 1);
-by (res_inst_tac [("t","%k.ys=r@a#k"),("s","%k.ys=(r@[a])@k")] subst 1);
+by (res_inst_tac [("t","%k. ys=r@a#k"),("s","%k. ys=(r@[a])@k")] subst 1);
  by (Simp_tac 1);
 by (Fast_tac 1);
 val step2_c = (result() repeat_RS spec) RS mp;
@@ -172,7 +172,7 @@
 "! st erk r p ys yss zs. \
 \  acc xs st erk r p A = (ys#yss, zs) --> \
 \  (if acc_prefix A st xs  \
-\   then ? g.ys=r@g & (!as. as<=xs & g<=as & g~=as --> ~fin A (nexts A st as))\
+\   then ? g. ys=r@g & (!as. as<=xs & g<=as & g~=as --> ~fin A (nexts A st as))\
 \   else (erk~=[] & ys=erk) | (erk=[] & (ys#yss,zs)=p))";
 by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
 by (list.induct_tac "xs" 1);
@@ -183,10 +183,10 @@
 by (case_tac "acc_prefix A (next A st a) list" 1);
  by (rtac conjI 1);
   by (strip_tac 1);
-  by (res_inst_tac [("f","%k.a#k")] ex_special 1);
-  by (res_inst_tac [("t","%k.ys=r@a#k"),("s","%k.ys=(r@[a])@k")] subst 1);
+  by (res_inst_tac [("f","%k. a#k")] ex_special 1);
+  by (res_inst_tac [("t","%k. ys=r@a#k"),("s","%k. ys=(r@[a])@k")] subst 1);
    by (Simp_tac 1);
-  by (res_inst_tac [("P","%k.ys = (r@[a])@k & (!as. as<=list & k<=as & k ~= as --> ~ fin A (nexts A (next A st a) as))")] exE 1);
+  by (res_inst_tac [("P","%k. ys = (r@[a])@k & (!as. as<=list & k<=as & k ~= as --> ~ fin A (nexts A (next A st a) as))")] exE 1);
    by (asm_simp_tac HOL_ss 1);
   by (res_inst_tac [("x","x")] exI 1);
   by (Asm_simp_tac 1);
@@ -194,10 +194,10 @@
    by (Simp_tac 1);
   by (asm_simp_tac (!simpset addcongs[conj_cong]) 1);
  by (strip_tac 1);
- by (res_inst_tac [("f","%k.a#k")] ex_special 1);
- by (res_inst_tac [("t","%k.ys=r@a#k"),("s","%k.ys=(r@[a])@k")] subst 1);
+ by (res_inst_tac [("f","%k. a#k")] ex_special 1);
+ by (res_inst_tac [("t","%k. ys=r@a#k"),("s","%k. ys=(r@[a])@k")] subst 1);
   by (Simp_tac 1);
- by (res_inst_tac [("P","%k.ys=(r@[a])@k & (!as. as<=list & k<=as & k~=as --> ~ fin A (nexts A (next A st a) as))")] exE 1);
+ by (res_inst_tac [("P","%k. ys=(r@[a])@k & (!as. as<=list & k<=as & k~=as --> ~ fin A (nexts A (next A st a) as))")] exE 1);
   by (asm_simp_tac HOL_ss 1);
  by (res_inst_tac [("x","x")] exI 1);
  by (Asm_simp_tac 1);
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/Lex/Prefix.ML
--- a/src/HOL/Lex/Prefix.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Lex/Prefix.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -6,7 +6,7 @@
 
 open Prefix;
 
-val [maj,min] = goal Prefix.thy "[| Q([]); !! y ys. Q(y#ys) |] ==> ! l.Q(l)";
+val [maj,min] = goal Prefix.thy "[| Q([]); !! y ys. Q(y#ys) |] ==> ! l. Q(l)";
 by (rtac allI 1);
 by (list.induct_tac "l" 1);
 by (rtac maj 1);
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/Lfp.ML
--- a/src/HOL/Lfp.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Lfp.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -41,7 +41,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);
@@ -66,7 +66,7 @@
 
 val rew::prems = goal Lfp.thy
     "[| A == lfp(f);  mono(f);   a:A;                   \
-\       !!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 22bbc1676768 -r b55686a7b22c src/HOL/List.ML
--- a/src/HOL/List.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/List.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -174,7 +174,7 @@
 by (ALLGOALS Asm_simp_tac);
 bind_thm("map_ext", impI RS (allI RS (result() RS mp)));
 
-goal thy "map (%x.x) = (%xs.xs)";
+goal thy "map (%x. x) = (%xs. xs)";
 by (rtac ext 1);
 by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
@@ -235,7 +235,7 @@
 qed "mem_append";
 Addsimps[mem_append];
 
-goal thy "x mem [x:xs.P(x)] = (x mem xs & P(x))";
+goal thy "x mem [x:xs. P(x)] = (x mem xs & P(x))";
 by (induct_tac "xs" 1);
 by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
 qed "mem_filter";
@@ -285,7 +285,7 @@
 
 section "list_all";
 
-goal thy "list_all (%x.True) xs = True";
+goal thy "list_all (%x. True) xs = True";
 by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "list_all_True";
@@ -599,7 +599,7 @@
 Addsimps [takeWhile_append1];
 
 goal thy
-  "(!x:set xs.P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys";
+  "(!x:set xs. P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys";
 by (induct_tac "xs" 1);
  by (Simp_tac 1);
 by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
@@ -616,7 +616,7 @@
 Addsimps [dropWhile_append1];
 
 goal thy
-  "(!x:set xs.P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys";
+  "(!x:set xs. P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys";
 by (induct_tac "xs" 1);
  by (Simp_tac 1);
 by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/List.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -38,7 +38,7 @@
 translations
   "[x, xs]"     == "x#[xs]"
   "[x]"         == "x#[]"
-  "[x:xs . P]"  == "filter (%x.P) xs"
+  "[x:xs . P]"  == "filter (%x. P) xs"
 
 syntax (symbols)
   "@filter"   :: [idt, 'a list, bool] => 'a list          ("(1[_\\<in>_ ./ _])")
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/MiniML/Instance.ML
--- a/src/HOL/MiniML/Instance.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/MiniML/Instance.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -211,7 +211,7 @@
 
 goalw thy [le_type_scheme_def,is_bound_typ_instance] "sch <= BVar n";
 by (strip_tac 1);
-by (res_inst_tac [("x","%a.t")]exI 1);
+by (res_inst_tac [("x","%a. t")]exI 1);
 by (Simp_tac 1);
 qed "bound_typ_instance_BVar";
 AddIffs [bound_typ_instance_BVar];
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/MiniML/Maybe.thy
--- a/src/HOL/MiniML/Maybe.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/MiniML/Maybe.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -13,6 +13,6 @@
   "option_bind m f == case m of None => None | Some r => f r"
 
 syntax "@option_bind" :: [pttrns,'a option,'b] => 'c ("(_ := _;//_)" 0)
-translations "P := E; F" == "option_bind E (%P.F)"
+translations "P := E; F" == "option_bind E (%P. F)"
 
 end
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/MiniML/Type.ML
--- a/src/HOL/MiniML/Type.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/MiniML/Type.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -16,7 +16,7 @@
 by (Fast_tac 1);
 qed_spec_mp "mk_scheme_Fun";
 
-goal thy "!t'.mk_scheme t = mk_scheme t' --> t=t'";
+goal thy "!t'. mk_scheme t = mk_scheme t' --> t=t'";
 by (typ.induct_tac "t" 1);
  by (rtac allI 1);
  by (typ.induct_tac "t'" 1);
@@ -110,14 +110,14 @@
 Addsimps[new_tv_id_subst];
 
 goal thy "new_tv n (sch::type_scheme) --> \
-\              $(%k.if k<n then S k else S' k) sch = $S sch";
+\              $(%k. if k<n then S k else S' k) sch = $S sch";
 by (type_scheme.induct_tac "sch" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "new_if_subst_type_scheme";
 Addsimps [new_if_subst_type_scheme];
 
 goal thy "new_tv n (A::type_scheme list) --> \
-\              $(%k.if k<n then S k else S' k) A = $S A";
+\              $(%k. if k<n then S k else S' k) A = $S A";
 by (list.induct_tac "A" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "new_if_subst_type_scheme_list";
@@ -673,7 +673,7 @@
 
 (* application of id_subst does not change type expression *)
 goalw thy [id_subst_def]
-  "$ id_subst = (%t::typ.t)";
+  "$ id_subst = (%t::typ. t)";
 by (rtac ext 1);
 by (typ.induct_tac "t" 1);
 by (ALLGOALS Asm_simp_tac);
@@ -681,7 +681,7 @@
 Addsimps [app_subst_id_te];
 
 goalw thy [id_subst_def]
-  "$ id_subst = (%sch::type_scheme.sch)";
+  "$ id_subst = (%sch::type_scheme. sch)";
 by (rtac ext 1);
 by (type_scheme.induct_tac "t" 1);
 by (ALLGOALS Asm_simp_tac);
@@ -690,7 +690,7 @@
 
 (* application of id_subst does not change list of type expressions *)
 goalw thy [app_subst_list]
-  "$ id_subst = (%A::type_scheme list.A)";
+  "$ id_subst = (%A::type_scheme list. A)";
 by (rtac ext 1); 
 by (list.induct_tac "A" 1);
 by (ALLGOALS Asm_simp_tac);
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/MiniML/Type.thy
--- a/src/HOL/MiniML/Type.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/MiniML/Type.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -112,7 +112,7 @@
 (* identity *)
 constdefs
         id_subst :: subst
-        "id_subst == (%n.TVar n)"
+        "id_subst == (%n. TVar n)"
 
 (* extension of substitution to type structures *)
 consts
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/MiniML/W.ML
--- a/src/HOL/MiniML/W.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/MiniML/W.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -485,7 +485,7 @@
 (* case Abs e *)
 by (strip_tac 1);
 by (eresolve_tac has_type_casesE 1);
-by (eres_inst_tac [("x","%x.if x=n then t1 else (S' x)")] allE 1);
+by (eres_inst_tac [("x","%x. if x=n then t1 else (S' x)")] allE 1);
 by (eres_inst_tac [("x","(FVar n)#A")] allE 1);
 by (eres_inst_tac [("x","t2")] allE 1);
 by (eres_inst_tac [("x","Suc n")] allE 1);
@@ -515,9 +515,9 @@
         conjunct1,new_scheme_list_le,new_tv_subst_scheme_list]) 1);
 (** LEVEL 35 **)
 by (subgoal_tac
-  "$ (%x.if x=ma then t' else (if x:(free_tv t - free_tv Sa) then R x \
+  "$ (%x. if x=ma then t' else (if x:(free_tv t - free_tv Sa) then R x \
 \        else Ra x)) ($ Sa t) = \
-\  $ (%x.if x=ma then t' else (if x:(free_tv t - free_tv Sa) then R x \
+\  $ (%x. if x=ma then t' else (if x:(free_tv t - free_tv Sa) then R x \
 \        else Ra x)) (ta -> (TVar ma))" 1);
 by (res_inst_tac [("t","$ (%x. if x = ma then t' else \
 \   (if x:(free_tv t - free_tv Sa) then R x else Ra x)) ($ Sa t)"),
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/Modelcheck/MuCalculus.thy
--- a/src/HOL/Modelcheck/MuCalculus.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Modelcheck/MuCalculus.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -18,7 +18,7 @@
 
 defs 
 
-Charfun_def      "Charfun     == (% A.% x.x:A)"
+Charfun_def      "Charfun     == (% A.% x. x:A)"
 monoP_def        "monoP f     == mono(Collect o f o Charfun)"
 mu_def           "mu f        == Charfun(lfp(Collect o f o Charfun))"
 nu_def           "nu f        == Charfun(gfp(Collect o f o Charfun))"
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/NatDef.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -585,14 +585,14 @@
 qed "Least_nat_def";
 
 val [prem1,prem2] = goalw thy [Least_nat_def]
-    "[| P(k::nat);  !!x. x<k ==> ~P(x) |] ==> (LEAST x.P(x)) = k";
+    "[| P(k::nat);  !!x. x<k ==> ~P(x) |] ==> (LEAST x. P(x)) = k";
 by (rtac select_equality 1);
 by (blast_tac (!claset addSIs [prem1,prem2]) 1);
 by (cut_facts_tac [less_linear] 1);
 by (blast_tac (!claset addSIs [prem1] addSDs [prem2]) 1);
 qed "Least_equality";
 
-val [prem] = goal thy "P(k::nat) ==> P(LEAST x.P(x))";
+val [prem] = goal thy "P(k::nat) ==> P(LEAST x. P(x))";
 by (rtac (prem RS rev_mp) 1);
 by (res_inst_tac [("n","k")] less_induct 1);
 by (rtac impI 1);
@@ -604,7 +604,7 @@
 qed "LeastI";
 
 (*Proof is almost identical to the one above!*)
-val [prem] = goal thy "P(k::nat) ==> (LEAST x.P(x)) <= k";
+val [prem] = goal thy "P(k::nat) ==> (LEAST x. P(x)) <= k";
 by (rtac (prem RS rev_mp) 1);
 by (res_inst_tac [("n","k")] less_induct 1);
 by (rtac impI 1);
@@ -615,7 +615,7 @@
 by (blast_tac (!claset addIs [less_imp_le,le_trans]) 1);
 qed "Least_le";
 
-val [prem] = goal thy "k < (LEAST x.P(x)) ==> ~P(k::nat)";
+val [prem] = goal thy "k < (LEAST x. P(x)) ==> ~P(k::nat)";
 by (rtac notI 1);
 by (etac (rewrite_rule [le_def] Least_le RS notE) 1);
 by (rtac prem 1);
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/NatDef.thy
--- a/src/HOL/NatDef.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/NatDef.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -56,7 +56,7 @@
 translations
    "1"  == "Suc 0"
    "2"  == "Suc 1"
-  "case p of 0 => a | Suc y => b" == "nat_case a (%y.b) p"
+  "case p of 0 => a | Suc y => b" == "nat_case a (%y. b) p"
 
 
 defs
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Prod.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -88,7 +88,7 @@
 !!a b. ... = ?P(a,b)
 which cannot be solved by reflexivity.
    
-val [prem] = goal Prod.thy "(!!x.PROP P x) ==> (!!a b. PROP P(a,b))";
+val [prem] = goal Prod.thy "(!!x. PROP P x) ==> (!!a b. PROP P(a,b))";
 br prem 1;
 val lemma1 = result();
 
@@ -226,7 +226,7 @@
 by (asm_simp_tac (!simpset addsimps [prod_fun,o_def]) 1);
 qed "prod_fun_compose";
 
-goal Prod.thy "prod_fun (%x.x) (%y.y) = (%z.z)";
+goal Prod.thy "prod_fun (%x. x) (%y. y) = (%z. z)";
 by (rtac ext 1);
 by (res_inst_tac [("p","z")] PairE 1);
 by (asm_simp_tac (!simpset addsimps [prod_fun]) 1);
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/Prod.thy
--- a/src/HOL/Prod.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Prod.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -52,17 +52,17 @@
   "@Times"      :: "['a set, 'a => 'b set] => ('a * 'b) set"    ("_ Times _" [81, 80] 80)
 
 translations
-  "(x, y, z)"   == "(x, (y, z))"
-  "(x, y)"      == "Pair x y"
+  "(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,zs).b"  == "split(%x (y,zs).b)"
+  "%(x,y).b"     == "split(%x y. b)"
   "_abs (Pair x y) t" => "%(x,y).t"
   (* The last rule accommodates tuples in `case C ... (x,y) ... => ...'
      The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *)
 
-  "SIGMA x:A.B" => "Sigma A (%x.B)"
-  "A Times B"   => "Sigma A (_K B)"
+  "SIGMA x:A. B" => "Sigma A (%x. B)"
+  "A Times B"    => "Sigma A (_K B)"
 
 syntax (symbols)
   "@Sigma"      :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"   ("(3\\<Sigma> _\\<in>_./ _)" 10)
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/Quot/FRACT.ML
--- a/src/HOL/Quot/FRACT.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Quot/FRACT.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -7,7 +7,7 @@
 open FRACT;
 
 goalw thy [per_def,per_NP_def]
-"(op ===)=(%x y.fst(rep_NP x)*snd(rep_NP y)=fst(rep_NP y)*snd(rep_NP x))";
+"(op ===)=(%x y. fst(rep_NP x)*snd(rep_NP y)=fst(rep_NP y)*snd(rep_NP x))";
 fr refl;
 qed "inst_NP_per";
 
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/Quot/HQUOT.ML
--- a/src/HOL/Quot/HQUOT.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Quot/HQUOT.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -7,7 +7,7 @@
 open HQUOT;
 
 (* first prove some helpful lemmas *)
-goalw thy [quot_def] "{y.y===x}:quot";
+goalw thy [quot_def] "{y. y===x}:quot";
 by (Asm_simp_tac 1);
 by (fast_tac (set_cs addIs [per_sym]) 1);
 qed "per_class_rep_quot";
@@ -20,7 +20,7 @@
 qed "quot_eq";
 
 (* prepare induction and exhaustiveness *)
-val prems = goal thy "!s.s:quot --> P (Abs_quot s) ==> P x";
+val prems = goal thy "!s. s:quot --> P (Abs_quot s) ==> P x";
 by (cut_facts_tac prems 1);
 by (rtac (Abs_quot_inverse RS subst) 1);
 by (rtac Rep_quot 1);
@@ -28,7 +28,7 @@
 by (asm_full_simp_tac (HOL_ss addsimps [Rep_quot,Rep_quot_inverse]) 1);
 qed "all_q";
 
-goal thy "? s.s:quot & x=Abs_quot s";
+goal thy "? s. s:quot & x=Abs_quot s";
 by (res_inst_tac [("x","Rep_quot x")] exI 1);
 by (asm_full_simp_tac (HOL_ss addsimps [Rep_quot,Rep_quot_inverse]) 1);
 qed "exh_q";
@@ -113,7 +113,7 @@
 qed "er_class_not";
 
 (* exhaustiveness and induction *)
-goalw thy [peclass_def] "? s.x=<[s]>";
+goalw thy [peclass_def] "? s. x=<[s]>";
 by (rtac all_q 1);
 by (strip_tac 1);
 by (asm_full_simp_tac (HOL_ss addsimps [mem_Collect_eq,quot_def]) 1);
@@ -128,7 +128,7 @@
 by (fast_tac set_cs 1);
 qed "per_class_exh";
 
-val prems = goal thy "!x.P<[x]> ==> P s";
+val prems = goal thy "!x. P<[x]> ==> P s";
 by (cut_facts_tac (prems@[
 	read_instantiate[("x","s::'a::per quot")] per_class_exh]) 1);
 by (fast_tac set_cs 1);
@@ -160,7 +160,7 @@
 qed "er_class_any_in";
 
 (* equivalent theorem for per would need !x.x:D *)
-val prems = goal thy "!x::'a::per.x:D==><[any_in (q::'a::per quot)]> = q";
+val prems = goal thy "!x::'a::per. x:D==><[any_in (q::'a::per quot)]> = q";
 by (cut_facts_tac prems 1);
 fr per_class_all;
 fr allI;
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/Quot/HQUOT.thy
--- a/src/HOL/Quot/HQUOT.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Quot/HQUOT.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -9,7 +9,7 @@
 
 HQUOT = PER +      
 
-typedef 'a quot = "{s::'a::per set. ? r.!y.y:s=y===r}" (quotNE)
+typedef 'a quot = "{s::'a::per set. ? r.!y. y:s=y===r}" (quotNE)
 
 (* constants for equivalence classes *)
 consts
@@ -21,7 +21,7 @@
 translations    "<[x]>" == "peclass x"
 
 defs
-        peclass_def     "<[x]> == Abs_quot {y.y===x}"
+        peclass_def     "<[x]> == Abs_quot {y. y===x}"
         any_in_def      "any_in f == @x.<[x]>=f"
 end
 
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/Quot/NPAIR.thy
--- a/src/HOL/Quot/NPAIR.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Quot/NPAIR.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -18,7 +18,7 @@
 
 (* NPAIR (continued) *)
 defs	per_NP_def 
-  "eqv ==(%x y.fst(rep_NP x)*snd(rep_NP y)=fst(rep_NP y)*snd(rep_NP x))"
+  "eqv ==(%x y. fst(rep_NP x)*snd(rep_NP y)=fst(rep_NP y)*snd(rep_NP x))"
 
 (* for proves of this rule see [Slo97diss] *)
 rules
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/Quot/PER.ML
--- a/src/HOL/Quot/PER.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Quot/PER.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -6,12 +6,12 @@
 *)
 open PER;
 
-goalw thy [fun_per_def,per_def] "f===g=(!x y.x:D&y:D&x===y-->f x===g y)";
+goalw thy [fun_per_def,per_def] "f===g=(!x y. x:D&y:D&x===y-->f x===g y)";
 by (rtac refl 1);
 qed "inst_fun_per";
 
 (* Witness that quot is not empty *)
-goal thy "?z:{s.? r.!y.y:s=y===r}";
+goal thy "?z:{s.? r.!y. y:s=y===r}";
 fr CollectI;
 by (res_inst_tac [("x","x")] exI 1);
 by (rtac allI 1);
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/Quot/PER0.thy
--- a/src/HOL/Quot/PER0.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Quot/PER0.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -27,9 +27,9 @@
         D         :: "'a::per set"
 defs
         per_def         "(op ===) == eqv"
-        Dom             "D=={x.x===x}"
+        Dom             "D=={x. x===x}"
 (* define ==== on and function type => *)
-        fun_per_def     "eqv f g == !x y.x:D & y:D & x===y --> f x === g y"
+        fun_per_def     "eqv f g == !x y. x:D & y:D & x===y --> f x === g y"
 
 syntax (symbols)
   "op ==="   :: "['a,'a::per] => bool"        (infixl "\\<sim>" 50)
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/Set.ML
--- a/src/HOL/Set.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Set.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -13,11 +13,11 @@
 Addsimps [Collect_mem_eq];
 AddIffs  [mem_Collect_eq];
 
-goal Set.thy "!!a. P(a) ==> a : {x.P(x)}";
+goal Set.thy "!!a. P(a) ==> a : {x. P(x)}";
 by (Asm_simp_tac 1);
 qed "CollectI";
 
-val prems = goal Set.thy "!!a. a : {x.P(x)} ==> P(a)";
+val prems = goal Set.thy "!!a. a : {x. P(x)} ==> P(a)";
 by (Asm_full_simp_tac 1);
 qed "CollectD";
 
@@ -67,7 +67,7 @@
 qed "bexI";
 
 qed_goal "bexCI" Set.thy 
-   "[| ! x:A. ~P(x) ==> P(a);  a:A |] ==> ? x:A.P(x)"
+   "[| ! x:A. ~P(x) ==> P(a);  a:A |] ==> ? x:A. P(x)"
  (fn prems=>
   [ (rtac classical 1),
     (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1))  ]);
@@ -82,12 +82,12 @@
 AddSEs [bexE];
 
 (*Trival rewrite rule*)
-goal Set.thy "(! x:A.P) = ((? x. x:A) --> P)";
+goal Set.thy "(! x:A. P) = ((? x. x:A) --> P)";
 by (simp_tac (!simpset addsimps [Ball_def]) 1);
 qed "ball_triv";
 
 (*Dual form for existentials*)
-goal Set.thy "(? x:A.P) = ((? x. x:A) & P)";
+goal Set.thy "(? x:A. P) = ((? x. x:A) & P)";
 by (simp_tac (!simpset addsimps [Bex_def]) 1);
 qed "bex_triv";
 
@@ -113,7 +113,7 @@
 
 section "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";
 
@@ -415,7 +415,7 @@
 AddSDs [singleton_inject];
 AddSEs [singletonE];
 
-goal Set.thy "{x.x=a} = {a}";
+goal Set.thy "{x. x=a} = {a}";
 by(Blast_tac 1);
 qed "singleton_conv";
 Addsimps [singleton_conv];
@@ -606,7 +606,7 @@
 
 (*The eta-expansion gives variable-name preservation.*)
 val major::prems = goalw thy [image_def]
-    "[| b : (%x.f(x))``A;  !!x.[| b=f(x);  x:A |] ==> P |] ==> P"; 
+    "[| b : (%x. f(x))``A;  !!x.[| b=f(x);  x:A |] ==> P |] ==> P"; 
 by (rtac (major RS CollectD RS bexE) 1);
 by (REPEAT (ares_tac prems 1));
 qed "imageE";
@@ -632,7 +632,7 @@
 bind_thm ("rangeI", UNIV_I RS imageI);
 
 val [major,minor] = goal thy 
-    "[| b : range(%x.f(x));  !!x. b=f(x) ==> P |] ==> P"; 
+    "[| b : range(%x. f(x));  !!x. b=f(x) ==> P |] ==> P"; 
 by (rtac (major RS imageE) 1);
 by (etac minor 1);
 qed "rangeE";
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/Set.thy
--- a/src/HOL/Set.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Set.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -125,8 +125,8 @@
 
   (* Isomorphisms between Predicates and Sets *)
 
-  mem_Collect_eq    "(a : {x.P(x)}) = P(a)"
-  Collect_mem_eq    "{x.x:A} = A"
+  mem_Collect_eq    "(a : {x. P(x)}) = P(a)"
+  Collect_mem_eq    "{x. x:A} = A"
 
 
 defs
@@ -136,18 +136,18 @@
   subset_def    "A <= B         == ! x:A. x:B"
   psubset_def   "A < B          == (A::'a set) <= B & ~ A=B"
   Compl_def     "Compl A        == {x. ~x:A}"
-  Un_def        "A Un B         == {x.x:A | x:B}"
-  Int_def       "A Int B        == {x.x:A & x:B}"
+  Un_def        "A Un B         == {x. x:A | x:B}"
+  Int_def       "A Int B        == {x. x:A & x:B}"
   set_diff_def  "A - B          == {x. x:A & ~x:B}"
   INTER_def     "INTER A B      == {y. ! x:A. y: B(x)}"
   UNION_def     "UNION A B      == {y. ? x:A. y: B(x)}"
-  INTER1_def    "INTER1 B       == INTER {x.True} B"
-  UNION1_def    "UNION1 B       == UNION {x.True} B"
+  INTER1_def    "INTER1 B       == INTER {x. True} B"
+  UNION1_def    "UNION1 B       == UNION {x. True} B"
   Inter_def     "Inter S        == (INT x:S. x)"
   Union_def     "Union S        == (UN x:S. x)"
   Pow_def       "Pow A          == {B. B <= A}"
   empty_def     "{}             == {x. False}"
-  insert_def    "insert a B     == {x.x=a} Un B"
+  insert_def    "insert a B     == {x. x=a} Un B"
   image_def     "f``A           == {y. ? x:A. y=f(x)}"
 
 end
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/Subst/AList.thy
--- a/src/HOL/Subst/AList.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Subst/AList.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -17,6 +17,6 @@
 
   alist_rec_def "alist_rec al b c == list_rec b (split c) al"
 
-  assoc_def   "assoc v d al == alist_rec al d (%x y xs g.if v=x then y else g)"
+  assoc_def   "assoc v d al == alist_rec al d (%x y xs g. if v=x then y else g)"
 
 end
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/Subst/Subst.ML
--- a/src/HOL/Subst/Subst.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Subst/Subst.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -34,7 +34,7 @@
 qed_spec_mp "Var_not_occs";
 
 goal Subst.thy
-    "(t <|r = t <|s) = (! v.v : vars_of(t) --> Var(v) <|r = Var(v) <|s)";
+    "(t <|r = t <|s) = (! v. v : vars_of(t) --> Var(v) <|r = Var(v) <|s)";
 by (induct_tac "t" 1);
 by (ALLGOALS Asm_full_simp_tac);
 by (ALLGOALS Blast_tac);
@@ -54,7 +54,7 @@
 
 (**** Equality between Substitutions ****)
 
-goalw Subst.thy [subst_eq_def] "r =$= s = (! t.t <| r = t <| s)";
+goalw Subst.thy [subst_eq_def] "r =$= s = (! t. t <| r = t <| s)";
 by (Simp_tac 1);
 qed "subst_eq_iff";
 
@@ -150,7 +150,7 @@
 
 
 goalw Subst.thy [srange_def]  
-   "v : srange(s) = (? w.w : sdom(s) & v : vars_of(Var(w) <| s))";
+   "v : srange(s) = (? w. w : sdom(s) & v : vars_of(Var(w) <| s))";
 by (Blast_tac 1);
 qed "srange_iff";
 
@@ -186,12 +186,12 @@
 qed_spec_mp "Var_intro";
 
 goal Subst.thy
-    "v : srange(s) --> (? w.w : sdom(s) & v : vars_of(Var(w) <| s))";
+    "v : srange(s) --> (? w. w : sdom(s) & v : vars_of(Var(w) <| s))";
 by (simp_tac (!simpset addsimps [srange_iff]) 1);
 qed_spec_mp "srangeD";
 
 goal Subst.thy
-   "sdom(s) Int srange(s) = {} = (! t.sdom(s) Int vars_of(t <| s) = {})";
+   "sdom(s) Int srange(s) = {} = (! t. sdom(s) Int vars_of(t <| s) = {})";
 by (simp_tac (!simpset addsimps [empty_iff_all_not]) 1);
 by (fast_tac (!claset addIs [Var_in_srange] addDs [srangeD]) 1);
 qed "dom_range_disjoint";
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/Subst/Subst.thy
--- a/src/HOL/Subst/Subst.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Subst/Subst.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -26,7 +26,7 @@
 
 defs 
 
-  subst_eq_def  "r =$= s == ALL t.t <| r = t <| s"
+  subst_eq_def  "r =$= s == ALL t. t <| r = t <| s"
 
   comp_def    "al <> bl == alist_rec al bl (%x y xs g. (x,y <| bl)#g)"
 
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/Sum.ML
--- a/src/HOL/Sum.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Sum.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -194,7 +194,7 @@
 by (etac IntD1 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";
 
@@ -203,6 +203,6 @@
 qed "Part_Int";
 
 (*For inductive definitions*)
-goal Sum.thy "Part (A Int {x.P x}) h = (Part A h) Int {x.P x}";
+goal Sum.thy "Part (A Int {x. P x}) h = (Part A h) Int {x. P x}";
 by (Blast_tac 1);
 qed "Part_Collect";
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/Sum.thy
--- a/src/HOL/Sum.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Sum.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -34,7 +34,7 @@
   Part          :: ['a set, 'b => 'a] => 'a set
 
 translations
-  "case p of Inl x => a | Inr y => b" == "sum_case (%x.a) (%y.b) p"
+  "case p of Inl x => a | Inr y => b" == "sum_case (%x. a) (%y. b) p"
 
 defs
   Inl_def       "Inl == (%a. Abs_Sum(Inl_Rep(a)))"
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/TLA/IntLemmas.ML
--- a/src/HOL/TLA/IntLemmas.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/TLA/IntLemmas.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -359,24 +359,24 @@
 
 
 qed_goal "allEW" Intensional.thy 
-         "[| RALL x.P(x);  P(x) ==> R |] ==> R::('w::world) form"
+         "[| RALL x. P(x);  P(x) ==> R |] ==> R::('w::world) form"
  (fn major::prems=>
   [ (REPEAT (resolve_tac (prems @ [major RS specW]) 1)) ]);
 
 qed_goal "all_dupEW" Intensional.thy 
-    "[| RALL x.P(x);  [| P(x); RALL x.P(x) |] ==> R |] ==> R::('w::world) form"
+    "[| RALL x. P(x);  [| P(x); RALL x. P(x) |] ==> R |] ==> R::('w::world) form"
  (fn prems =>
   [ (REPEAT (resolve_tac (prems @ (prems RL [specW])) 1)) ]);
 
 
-qed_goal "exIW" Intensional.thy "P(x) ==> REX x.P(x)"
+qed_goal "exIW" Intensional.thy "P(x) ==> REX x. P(x)"
   (fn [prem] => [rtac intI 1,
                  rewrite_goals_tac intensional_rews,
                  rtac exI 1,
                  rtac (prem RS intD) 1]);
 
 qed_goal "exEW" Intensional.thy 
-  "[| w |= REX x.P(x); !!x. P(x) .-> Q |] ==> w |= Q"
+  "[| w |= REX x. P(x); !!x. P(x) .-> Q |] ==> w |= Q"
   (fn [major,minor] => [rtac exE 1,
                         rtac (rewrite_rule intensional_rews major) 1,
                         etac rev_mpW 1,
@@ -385,7 +385,7 @@
 (** Classical quantifier reasoning **)
 
 qed_goal "exCIW" Intensional.thy 
-  "(w |= (RALL x. .~P(x)) .-> P(a)) ==> w |= REX x.P(x)"
+  "(w |= (RALL x. .~P(x)) .-> P(a)) ==> w |= REX x. P(x)"
   (fn prems => [cut_facts_tac prems 1,
                 rewrite_goals_tac intensional_rews,
                 fast_tac HOL_cs 1]);
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/TLA/Intensional.ML
--- a/src/HOL/TLA/Intensional.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/TLA/Intensional.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -35,7 +35,7 @@
    "(P .| #True) .= #True", "(#True .| P) .= #True", 
    "(P .| #False) .= P", "(#False .| P) .= P", 
    "(P .| P) .= P", "(P .| .~P) .= #True", "(.~P .| P) .= #True",
-   "(RALL x.P) .= P", "(REX x.P) .= P",
+   "(RALL x. P) .= P", "(REX x. P) .= P",
    "(.~Q .-> .~P) .= (P .-> Q)",
    "(P.|Q .-> R) .= ((P.->R).&(Q.->R))" ];
 
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/TLA/Stfun.ML
--- a/src/HOL/TLA/Stfun.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/TLA/Stfun.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -8,7 +8,7 @@
 
 (* A stronger version of existential elimination (goal needn't be boolean) *)
 qed_goalw "exE_prop" HOL.thy [Ex_def]
-  "[| ? x::'a.P(x); !!x. P(x) ==> PROP R |] ==> PROP R"
+  "[| ? x::'a. P(x); !!x. P(x) ==> PROP R |] ==> PROP R"
   (fn prems => [REPEAT(resolve_tac prems 1)]);
 
 (* Might as well use that version in automated proofs *)
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/Univ.ML
--- a/src/HOL/Univ.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/Univ.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -439,23 +439,23 @@
 
 (**** UN x. B(x) rules ****)
 
-goalw Univ.thy [ntrunc_def] "ntrunc k (UN x.f(x)) = (UN x. ntrunc k (f x))";
+goalw Univ.thy [ntrunc_def] "ntrunc k (UN x. f(x)) = (UN x. ntrunc k (f x))";
 by (Blast_tac 1);
 qed "ntrunc_UN1";
 
-goalw Univ.thy [Scons_def] "(UN x.f(x)) $ M = (UN x. f(x) $ M)";
+goalw Univ.thy [Scons_def] "(UN x. f(x)) $ M = (UN x. f(x) $ M)";
 by (Blast_tac 1);
 qed "Scons_UN1_x";
 
-goalw Univ.thy [Scons_def] "M $ (UN x.f(x)) = (UN x. M $ f(x))";
+goalw Univ.thy [Scons_def] "M $ (UN x. f(x)) = (UN x. M $ f(x))";
 by (Blast_tac 1);
 qed "Scons_UN1_y";
 
-goalw Univ.thy [In0_def] "In0(UN x.f(x)) = (UN x. In0(f(x)))";
+goalw Univ.thy [In0_def] "In0(UN x. f(x)) = (UN x. In0(f(x)))";
 by (rtac Scons_UN1_y 1);
 qed "In0_UN1";
 
-goalw Univ.thy [In1_def] "In1(UN x.f(x)) = (UN x. In1(f(x)))";
+goalw Univ.thy [In1_def] "In1(UN x. f(x)) = (UN x. In1(f(x)))";
 by (rtac Scons_UN1_y 1);
 qed "In1_UN1";
 
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/W0/Maybe.thy
--- a/src/HOL/W0/Maybe.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/W0/Maybe.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -15,6 +15,6 @@
   "m bind f == case m of Ok r => f r | Fail => Fail"
 
 syntax "@bind" :: [patterns,'a maybe,'b] => 'c ("(_ := _;//_)" 0)
-translations "P := E; F" == "E bind (%P.F)"
+translations "P := E; F" == "E bind (%P. F)"
 
 end
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/W0/Type.ML
--- a/src/HOL/W0/Type.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/W0/Type.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -15,7 +15,7 @@
 
 (* application of id_subst does not change type expression *)
 goalw thy [id_subst_def]
-  "$ id_subst = (%t::typ.t)";
+  "$ id_subst = (%t::typ. t)";
 by (rtac ext 1);
 by (typ.induct_tac "t" 1);
 by (ALLGOALS Asm_simp_tac);
@@ -24,7 +24,7 @@
 
 (* application of id_subst does not change list of type expressions *)
 goalw thy [app_subst_list]
-  "$ id_subst = (%ts::typ list.ts)";
+  "$ id_subst = (%ts::typ list. ts)";
 by (rtac ext 1); 
 by (list.induct_tac "ts" 1);
 by (ALLGOALS Asm_simp_tac);
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/W0/Type.thy
--- a/src/HOL/W0/Type.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/W0/Type.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -30,7 +30,7 @@
 (* identity *)
 constdefs
         id_subst :: subst
-        "id_subst == (%n.TVar n)"
+        "id_subst == (%n. TVar n)"
 
 (* extension of substitution to type structures *)
 consts
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/W0/W.ML
--- a/src/HOL/W0/W.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/W0/W.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -237,7 +237,7 @@
 (* case Abs e *)
 by (strip_tac 1);
 by (eresolve_tac has_type_casesE 1);
-by (eres_inst_tac [("x","%x.if x=n then t1 else (s' x)")] allE 1);
+by (eres_inst_tac [("x","%x. if x=n then t1 else (s' x)")] allE 1);
 by (eres_inst_tac [("x","(TVar n)#a")] allE 1);
 by (eres_inst_tac [("x","t2")] allE 1);
 by (eres_inst_tac [("x","Suc n")] allE 1);
@@ -268,9 +268,9 @@
 
 (** LEVEL 35 **)
 by (subgoal_tac
-  "$ (%x.if x=ma then t' else (if x:(free_tv t - free_tv sa) then r x \
+  "$ (%x. if x=ma then t' else (if x:(free_tv t - free_tv sa) then r x \
 \        else ra x)) ($ sa t) = \
-\  $ (%x.if x=ma then t' else (if x:(free_tv t - free_tv sa) then r x \
+\  $ (%x. if x=ma then t' else (if x:(free_tv t - free_tv sa) then r x \
 \        else ra x)) (ta -> (TVar ma))" 1);
 by (res_inst_tac [("t","$ (%x. if x = ma then t' else \
 \   (if x:(free_tv t - free_tv sa) then r x else ra x)) ($ sa t)"),
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/WF.thy
--- a/src/HOL/WF.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/WF.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -10,7 +10,7 @@
 
 constdefs
   wf         :: "('a * 'a)set => bool"
-  "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x.P(x)))"
+  "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))"
 
   acyclic :: "('a*'a)set => bool"
   "acyclic r == !x. (x,x) ~: r^+"
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/cladata.ML
--- a/src/HOL/cladata.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/cladata.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -68,7 +68,7 @@
 
 (*Better then ex1E for classical reasoner: needs no quantifier duplication!*)
 qed_goal "alt_ex1E" thy
-    "[| ?! x.P(x);                                              \
+    "[| ?! x. P(x);                                              \
 \       !!x. [| P(x);  ALL y y'. P(y) & P(y') --> y=y' |] ==> R  \
 \    |] ==> R"
  (fn major::prems =>
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/datatype.ML
--- a/src/HOL/datatype.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/datatype.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -341,7 +341,7 @@
       fun t_inducting ((_, name, types, vns, _) :: cs) =
         let
           val h = if null types then " P(" ^ name ^ ")"
-                  else " !!" ^ (space_implode " " vns) ^ "." ^
+                  else " !!" ^ (space_implode " " vns) ^ ". " ^
                     (assumpt (types, vns, false)) ^
                     "P(" ^ C_exp name vns ^ ")";
           val rest = t_inducting cs;
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/equalities.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -12,7 +12,7 @@
 
 section "{}";
 
-goal Set.thy "{x.False} = {}";
+goal Set.thy "{x. False} = {}";
 by (Blast_tac 1);
 qed "Collect_False_empty";
 Addsimps [Collect_False_empty];
@@ -118,7 +118,7 @@
 
 goalw Set.thy [image_def]
 "(%x. if P x then f x else g x) `` S                    \
-\ = (f `` ({x.x:S & P x})) Un (g `` ({x.x:S & ~(P x)}))";
+\ = (f `` ({x. x:S & P x})) Un (g `` ({x. x:S & ~(P x)}))";
 by (split_tac [expand_if] 1);
 by (Blast_tac 1);
 qed "if_image_distrib";
@@ -421,11 +421,11 @@
 by (Blast_tac 1);
 qed "INT1_insert_distrib";
 
-goal Set.thy "Union(range(f)) = (UN x.f(x))";
+goal Set.thy "Union(range(f)) = (UN x. f(x))";
 by (Blast_tac 1);
 qed "Union_range_eq";
 
-goal Set.thy "Inter(range(f)) = (INT x.f(x))";
+goal Set.thy "Inter(range(f)) = (INT x. f(x))";
 by (Blast_tac 1);
 qed "Inter_range_eq";
 
@@ -445,12 +445,12 @@
 by (Blast_tac 1);
 qed "INT_constant";
 
-goal Set.thy "(UN x.B) = B";
+goal Set.thy "(UN x. B) = B";
 by (Blast_tac 1);
 qed "UN1_constant";
 Addsimps[UN1_constant];
 
-goal Set.thy "(INT x.B) = B";
+goal Set.thy "(INT x. B) = B";
 by (Blast_tac 1);
 qed "INT1_constant";
 Addsimps[INT1_constant];
@@ -524,11 +524,11 @@
 (** These are not added to the default simpset because (a) they duplicate the
     body and (b) there are no similar rules for Int. **)
 
-goal Set.thy "(ALL x:A Un B.P x) = ((ALL x:A.P x) & (ALL x:B.P x))";
+goal Set.thy "(ALL x:A Un B. P x) = ((ALL x:A. P x) & (ALL x:B. P x))";
 by (Blast_tac 1);
 qed "ball_Un";
 
-goal Set.thy "(EX x:A Un B.P x) = ((EX x:A.P x) | (EX x:B.P x))";
+goal Set.thy "(EX x:A Un B. P x) = ((EX x:A. P x) | (EX x:B. P x))";
 by (Blast_tac 1);
 qed "bex_Un";
 
@@ -620,7 +620,7 @@
 by (Blast_tac 1);
 qed "set_eq_subset";
 
-goal Set.thy "A <= B =  (! t.t:A --> t:B)";
+goal Set.thy "A <= B =  (! t. t:A --> t:B)";
 by (Blast_tac 1);
 qed "subset_iff";
 
@@ -647,32 +647,32 @@
 in
 val UN1_simps = map prover 
                 ["(UN x. insert a (B x)) = insert a (UN x. B x)",
-                 "(UN x. A x Int B)  = ((UN x.A x) Int B)",
-                 "(UN x. A Int B x)  = (A Int (UN x.B x))",
-                 "(UN x. A x Un B)   = ((UN x.A x) Un B)",
-                 "(UN x. A Un B x)   = (A Un (UN x.B x))",
-                 "(UN x. A x - B)    = ((UN x.A x) - B)",
-                 "(UN x. A - B x)    = (A - (INT x.B x))"];
+                 "(UN x. A x Int B)  = ((UN x. A x) Int B)",
+                 "(UN x. A Int B x)  = (A Int (UN x. B x))",
+                 "(UN x. A x Un B)   = ((UN x. A x) Un B)",
+                 "(UN x. A Un B x)   = (A Un (UN x. B x))",
+                 "(UN x. A x - B)    = ((UN x. A x) - B)",
+                 "(UN x. A - B x)    = (A - (INT x. B x))"];
 
 val INT1_simps = map prover
                 ["(INT x. insert a (B x)) = insert a (INT x. B x)",
-                 "(INT x. A x Int B) = ((INT x.A x) Int B)",
-                 "(INT x. A Int B x) = (A Int (INT x.B x))",
-                 "(INT x. A x Un B)  = ((INT x.A x) Un B)",
-                 "(INT x. A Un B x)  = (A Un (INT x.B x))",
-                 "(INT x. A x - B)   = ((INT x.A x) - B)",
-                 "(INT x. A - B x)   = (A - (UN x.B x))"];
+                 "(INT x. A x Int B) = ((INT x. A x) Int B)",
+                 "(INT x. A Int B x) = (A Int (INT x. B x))",
+                 "(INT x. A x Un B)  = ((INT x. A x) Un B)",
+                 "(INT x. A Un B x)  = (A Un (INT x. B x))",
+                 "(INT x. A x - B)   = ((INT x. A x) - B)",
+                 "(INT x. A - B x)   = (A - (UN x. B x))"];
 
 val UN_simps = map prover 
-                ["(UN x:C. A x Int B)  = ((UN x:C.A x) Int B)",
-                 "(UN x:C. A Int B x)  = (A Int (UN x:C.B x))",
-                 "(UN x:C. A x - B)    = ((UN x:C.A x) - B)",
-                 "(UN x:C. A - B x)    = (A - (INT x:C.B x))"];
+                ["(UN x:C. A x Int B)  = ((UN x:C. A x) Int B)",
+                 "(UN x:C. A Int B x)  = (A Int (UN x:C. B x))",
+                 "(UN x:C. A x - B)    = ((UN x:C. A x) - B)",
+                 "(UN x:C. A - B x)    = (A - (INT x:C. B x))"];
 
 val INT_simps = map prover
                 ["(INT x:C. insert a (B x)) = insert a (INT x:C. B x)",
-                 "(INT x:C. A x Un B)  = ((INT x:C.A x) Un B)",
-                 "(INT x:C. A Un B x)  = (A Un (INT x:C.B x))"];
+                 "(INT x:C. A x Un B)  = ((INT x:C. A x) Un B)",
+                 "(INT x:C. A Un B x)  = (A Un (INT x:C. B x))"];
 
 (*The missing laws for bounded Unions and Intersections are conditional
   on the index set's being non-empty.  Thus they are probably NOT worth 
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/ex/MT.ML
--- a/src/HOL/ex/MT.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/ex/MT.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -66,7 +66,7 @@
 qed "lfp_elim2";
 
 val prems = goal MT.thy
-  " [| x:lfp(f); mono(f); !!y. y:f(lfp(f) Int {x.P(x)}) ==> P(y) |] ==> \
+  " [| x:lfp(f); mono(f); !!y. y:f(lfp(f) Int {x. P(x)}) ==> P(y) |] ==> \
 \   P(x)";
 by (cut_facts_tac prems 1);
 by (etac induct 1);
@@ -446,7 +446,7 @@
 val prems = goal MT.thy 
   " te |- e ===> t ==> \
 \   ( e = fn x1 => e1 --> \
-\     (? t1 t2.t=t_fun t1 t2 & te + {x1 |=> t1} |- e1 ===> t2) \
+\     (? t1 t2. t=t_fun t1 t2 & te + {x1 |=> t1} |- e1 ===> t2) \
 \   )";
 by (elab_e_elim_tac prems);
 qed "elab_fn_elim_lem";
@@ -538,11 +538,11 @@
 (* Elimination rule for hasty_rel *)
 
 val prems = goalw MT.thy [hasty_rel_def]
-  " [| !! c t.c isof t ==> P((v_const(c),t)); \
+  " [| !! c t. c isof t ==> P((v_const(c),t)); \
 \      !! te ev e t ve. \
 \        [| te |- fn ev => e ===> t; \
 \           ve_dom(ve) = te_dom(te); \
-\           !ev1.ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : hasty_rel \
+\           !ev1. ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : hasty_rel \
 \        |] ==> P((v_clos(<|ev,e,ve|>),t)); \
 \      (v,t) : hasty_rel \
 \   |] ==> P((v,t))";
@@ -558,11 +558,11 @@
 
 val prems = goal MT.thy 
   " [| (v,t) : hasty_rel; \
-\      !! c t.c isof t ==> P (v_const c) t; \
+\      !! c t. c isof t ==> P (v_const c) t; \
 \      !! te ev e t ve. \
 \        [| te |- fn ev => e ===> t; \
 \           ve_dom(ve) = te_dom(te); \
-\           !ev1.ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : hasty_rel \
+\           !ev1. ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : hasty_rel \
 \        |] ==> P (v_clos <|ev,e,ve|>) t \
 \   |] ==> P v t";
 by (res_inst_tac [("P","P")] infsys_p2 1);
@@ -602,7 +602,7 @@
 val prems = goalw MT.thy [hasty_env_def,hasty_def] 
   " v hasty t ==> \
 \   ! x e ve. \
-\     v=v_clos(<|x,e,ve|>) --> (? te.te |- fn x => e ===> t & ve hastyenv te)";
+\     v=v_clos(<|x,e,ve|>) --> (? te. te |- fn x => e ===> t & ve hastyenv te)";
 by (cut_facts_tac prems 1);
 by (rtac hasty_rel_elim 1);
 by (ALLGOALS (blast_tac (v_ext_cs HOL_cs)));
@@ -610,7 +610,7 @@
 
 goal MT.thy 
   "!!t. v_clos(<|ev,e,ve|>) hasty t ==>  \
-\       ? te.te |- fn ev => e ===> t & ve hastyenv te ";
+\       ? te. te |- fn ev => e ===> t & ve hastyenv te ";
 by (dtac hasty_elim_clos_lem 1);
 by (Blast_tac 1);
 qed "hasty_elim_clos";
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/ex/MT.thy
--- a/src/HOL/ex/MT.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/ex/MT.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -247,7 +247,7 @@
      ve_dom(ve) = te_dom(te) & 
      ( ! x. 
          x:ve_dom(ve) --> 
-         (? c.ve_app ve x = v_const(c) & c isof te_app te x) 
+         (? c. ve_app ve x = v_const(c) & c isof te_app te x) 
      ) 
    "
 
@@ -263,7 +263,7 @@
            p = (v_clos(<|ev,e,ve|>),t) & 
            te |- fn ev => e ===> t & 
            ve_dom(ve) = te_dom(te) & 
-           (! ev1.ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : r) 
+           (! ev1. ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : r) 
        ) 
      } 
    "
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/ex/NatSum.ML
--- a/src/HOL/ex/NatSum.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/ex/NatSum.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -11,7 +11,7 @@
 Addsimps [add_mult_distrib, add_mult_distrib2];
 
 (*The sum of the first n positive integers equals n(n+1)/2.*)
-goal NatSum.thy "2*sum (%i.i) (Suc n) = n*Suc(n)";
+goal NatSum.thy "2*sum (%i. i) (Suc n) = n*Suc(n)";
 by (Simp_tac 1);
 by (nat_ind_tac "n" 1);
 by (Simp_tac 1);
@@ -19,7 +19,7 @@
 qed "sum_of_naturals";
 
 goal NatSum.thy
-  "Suc(Suc(Suc(Suc 2)))*sum (%i.i*i) (Suc n) = n*Suc(n)*Suc(2*n)";
+  "Suc(Suc(Suc(Suc 2)))*sum (%i. i*i) (Suc n) = n*Suc(n)*Suc(2*n)";
 by (Simp_tac 1);
 by (nat_ind_tac "n" 1);
 by (Simp_tac 1);
@@ -27,7 +27,7 @@
 qed "sum_of_squares";
 
 goal NatSum.thy
-  "Suc(Suc 2)*sum (%i.i*i*i) (Suc n) = n*n*Suc(n)*Suc(n)";
+  "Suc(Suc 2)*sum (%i. i*i*i) (Suc n) = n*n*Suc(n)*Suc(n)";
 by (Simp_tac 1);
 by (nat_ind_tac "n" 1);
 by (Simp_tac 1);
@@ -35,7 +35,7 @@
 qed "sum_of_cubes";
 
 (*The sum of the first n odd numbers equals n squared.*)
-goal NatSum.thy "sum (%i.Suc(i+i)) n = n*n";
+goal NatSum.thy "sum (%i. Suc(i+i)) n = n*n";
 by (nat_ind_tac "n" 1);
 by (Simp_tac 1);
 by (Asm_simp_tac 1);
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/ex/Puzzle.ML
--- a/src/HOL/ex/Puzzle.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/ex/Puzzle.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -9,7 +9,7 @@
 *)
 
 (*specialized form of induction needed below*)
-val prems = goal Nat.thy "[| P(0); !!n. P(Suc(n)) |] ==> !n.P(n)";
+val prems = goal Nat.thy "[| P(0); !!n. P(Suc(n)) |] ==> !n. P(n)";
 by (EVERY1 [rtac (nat_induct RS allI), resolve_tac prems, resolve_tac prems]);
 qed "nat_exh";
 
@@ -35,7 +35,7 @@
 by (deepen_tac (!claset addIs [Puzzle.f_ax, le_less_trans, lemma1]) 0 1);
 qed "lemma2";
 
-val prems = goal Puzzle.thy "(!!n.f(n) <= f(Suc(n))) ==> m<n --> f(m) <= f(n)";
+val prems = goal Puzzle.thy "(!!n. f(n) <= f(Suc(n))) ==> m<n --> f(m) <= f(n)";
 by (res_inst_tac[("n","n")]nat_induct 1);
 by (Simp_tac 1);
 by (simp_tac (!simpset addsimps [less_Suc_eq]) 1);
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/ex/Qsort.ML
--- a/src/HOL/ex/Qsort.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/ex/Qsort.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -35,7 +35,7 @@
 Addsimps [set_qsort];
 
 goal List.thy
-  "(!x:set[x:xs.P(x)].Q(x)) = (!x:set xs. P(x)-->Q(x))";
+  "(!x:set[x:xs. P(x)].Q(x)) = (!x:set xs. P(x)-->Q(x))";
 by (list.induct_tac "xs" 1);
 by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
 qed"Ball_set_filter";
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/ex/Recdef.thy
--- a/src/HOL/ex/Recdef.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/ex/Recdef.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -94,9 +94,9 @@
    TFL requires (%x.mapf x) instead of mapf.
 *)
 consts mapf :: nat => nat list
-recdef mapf "measure(%m.m)"
+recdef mapf "measure(%m. m)"
 congs "[map_cong]"
 "mapf 0 = []"
-"mapf (Suc n) = concat(map (%x.mapf x) (replicate n n))"
+"mapf (Suc n) = concat(map (%x. mapf x) (replicate n n))"
 
 end
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/ex/Sorting.ML
--- a/src/HOL/ex/Sorting.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/ex/Sorting.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -6,12 +6,12 @@
 Some general lemmas
 *)
 
-goal Sorting.thy "!x.mset (xs@ys) x = mset xs x + mset ys x";
+goal Sorting.thy "!x. mset (xs@ys) x = mset xs x + mset ys x";
 by (list.induct_tac "xs" 1);
 by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
 qed "mset_append";
 
-goal Sorting.thy "!x. mset [x:xs. ~p(x)] x + mset [x:xs.p(x)] x = \
+goal Sorting.thy "!x. mset [x:xs. ~p(x)] x + mset [x:xs. p(x)] x = \
 \                     mset xs x";
 by (list.induct_tac "xs" 1);
 by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
@@ -19,7 +19,7 @@
 
 Addsimps [mset_append, mset_compl_add];
 
-goal Sorting.thy "set xs = {x.mset xs x ~= 0}";
+goal Sorting.thy "set xs = {x. mset xs x ~= 0}";
 by (list.induct_tac "xs" 1);
 by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
 by (Fast_tac 1);
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/ex/cla.ML
--- a/src/HOL/ex/cla.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/ex/cla.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -129,15 +129,15 @@
 by (Blast_tac 1);
 result(); 
 
-goal HOL.thy "(? x. P-->Q(x))  =  (P --> (? x.Q(x)))";
+goal HOL.thy "(? x. P-->Q(x))  =  (P --> (? x. Q(x)))";
 by (Blast_tac 1);
 result(); 
 
-goal HOL.thy "(? x.P(x)-->Q) = ((! x.P(x)) --> Q)";
+goal HOL.thy "(? x. P(x)-->Q) = ((! x. P(x)) --> Q)";
 by (Blast_tac 1);
 result(); 
 
-goal HOL.thy "((! x.P(x)) | Q)  =  (! x. P(x) | Q)";
+goal HOL.thy "((! x. P(x)) | Q)  =  (! x. P(x) | Q)";
 by (Blast_tac 1);
 result(); 
 
@@ -204,7 +204,7 @@
 
 writeln"Problem 24";
 goal HOL.thy "~(? x. S(x)&Q(x)) & (! x. P(x) --> Q(x)|R(x)) &  \
-\    (~(? x.P(x)) --> (? x.Q(x))) & (! x. Q(x)|R(x) --> S(x))  \
+\    (~(? x. P(x)) --> (? x. Q(x))) & (! x. Q(x)|R(x) --> S(x))  \
 \   --> (? x. P(x)&R(x))";
 by (Blast_tac 1); 
 result();
@@ -237,7 +237,7 @@
 writeln"Problem 28.  AMENDED";
 goal HOL.thy "(! x. P(x) --> (! x. Q(x))) &   \
 \       ((! x. Q(x)|R(x)) --> (? x. Q(x)&S(x))) &  \
-\       ((? x.S(x)) --> (! x. L(x) --> M(x)))  \
+\       ((? x. S(x)) --> (! x. L(x) --> M(x)))  \
 \   --> (! x. P(x) & L(x) --> M(x))";
 by (Blast_tac 1);  
 result();
@@ -257,7 +257,7 @@
 result();
 
 writeln"Problem 31";
-goal HOL.thy "~(? x.P(x) & (Q(x) | R(x))) & \
+goal HOL.thy "~(? x. P(x) & (Q(x) | R(x))) & \
 \       (? x. L(x) & P(x)) & \
 \       (! x. ~ R(x) --> M(x))  \
 \   --> (? x. L(x) & M(x))";
@@ -303,7 +303,7 @@
 
 writeln"Problem 37";
 goal HOL.thy "(! z. ? w. ! x. ? y. \
-\          (P x z -->P y w) & P y z & (P y w --> (? u.Q u w))) & \
+\          (P x z -->P y w) & P y z & (P y w --> (? u. Q u w))) & \
 \       (! x z. ~(P x z) --> (? y. Q y z)) & \
 \       ((? x y. Q x y) --> (! x. R x x))  \
 \   --> (! x. ? y. R x y)";
@@ -380,7 +380,7 @@
 (*Hard because it involves substitution for Vars;
   the type constraint ensures that x,y,z have the same type as a,b,u. *)
 goal HOL.thy "(? x y::'a. ! z. z=x | z=y) & P(a) & P(b) & (~a=b) \
-\               --> (! u::'a.P(u))";
+\               --> (! u::'a. P(u))";
 by (Classical.safe_tac (!claset));
 by (res_inst_tac [("x","a")] allE 1);
 by (assume_tac 1);
@@ -391,7 +391,7 @@
 
 writeln"Problem 50";  
 (*What has this to do with equality?*)
-goal HOL.thy "(! x. P a x | (! y.P x y)) --> (? x. ! y.P x y)";
+goal HOL.thy "(! x. P a x | (! y. P x y)) --> (? x. ! y. P x y)";
 by (Blast_tac 1);
 result();
 
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/ex/meson.ML
--- a/src/HOL/ex/meson.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/ex/meson.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -25,8 +25,8 @@
 val not_conjD = prove_fun "~(P&Q) ==> ~P | ~Q";
 val not_disjD = prove_fun "~(P|Q) ==> ~P & ~Q";
 val not_notD = prove_fun "~~P ==> P";
-val not_allD = prove_fun  "~(! x.P(x)) ==> ? x. ~P(x)";
-val not_exD = prove_fun   "~(? x.P(x)) ==> ! x. ~P(x)";
+val not_allD = prove_fun  "~(! x. P(x)) ==> ? x. ~P(x)";
+val not_exD = prove_fun   "~(? x. P(x)) ==> ! x. ~P(x)";
 
 
 (*** Removal of --> and <-> (positive and negative occurrences) ***)
@@ -44,17 +44,17 @@
 
 (*** Conjunction ***)
 
-val conj_exD1 = prove_fun "(? x.P(x)) & Q ==> ? x. P(x) & Q";
-val conj_exD2 = prove_fun "P & (? x.Q(x)) ==> ? x. P & Q(x)";
+val conj_exD1 = prove_fun "(? x. P(x)) & Q ==> ? x. P(x) & Q";
+val conj_exD2 = prove_fun "P & (? x. Q(x)) ==> ? x. P & Q(x)";
 
 (*** Disjunction ***)
 
 (*DO NOT USE with forall-Skolemization: makes fewer schematic variables!!
   With ex-Skolemization, makes fewer Skolem constants*)
-val disj_exD = prove_fun "(? x.P(x)) | (? x.Q(x)) ==> ? x. P(x) | Q(x)";
+val disj_exD = prove_fun "(? x. P(x)) | (? x. Q(x)) ==> ? x. P(x) | Q(x)";
 
-val disj_exD1 = prove_fun "(? x.P(x)) | Q ==> ? x. P(x) | Q";
-val disj_exD2 = prove_fun "P | (? x.Q(x)) ==> ? x. P | Q(x)";
+val disj_exD1 = prove_fun "(? x. P(x)) | Q ==> ? x. P(x) | Q";
+val disj_exD2 = prove_fun "P | (? x. Q(x)) ==> ? x. P | Q(x)";
 
 
 (**** Skolemization -- pulling "?" over "!" ****)
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/ex/mesontest.ML
--- a/src/HOL/ex/mesontest.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/ex/mesontest.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -247,15 +247,15 @@
 by (safe_meson_tac 1);
 result(); 
 
-goal HOL.thy "(? x. P --> Q x)  =  (P --> (? x.Q x))";
+goal HOL.thy "(? x. P --> Q x)  =  (P --> (? x. Q x))";
 by (safe_meson_tac 1);
 result(); 
 
-goal HOL.thy "(? x.P x --> Q) = ((! x.P x) --> Q)";
+goal HOL.thy "(? x. P x --> Q) = ((! x. P x) --> Q)";
 by (safe_meson_tac 1);
 result(); 
 
-goal HOL.thy "((! x.P x) | Q)  =  (! x. P x | Q)";
+goal HOL.thy "((! x. P x) | Q)  =  (! x. P x | Q)";
 by (safe_meson_tac 1);
 result(); 
 
@@ -307,7 +307,7 @@
 
 writeln"Problem 24";  (*The first goal clause is useless*)
 goal HOL.thy "~(? x. S x & Q x) & (! x. P x --> Q x | R x) &  \
-\    (~(? x.P x) --> (? x.Q x)) & (! x. Q x | R x --> S x)  \
+\    (~(? x. P x) --> (? x. Q x)) & (! x. Q x | R x --> S x)  \
 \   --> (? x. P x & R x)";
 by (safe_meson_tac 1); 
 result();
@@ -340,7 +340,7 @@
 writeln"Problem 28.  AMENDED";  (*14 Horn clauses*)
 goal HOL.thy "(! x. P x --> (! x. Q x)) &   \
 \       ((! x. Q x | R x) --> (? x. Q x & S x)) &  \
-\       ((? x.S x) --> (! x. L x --> M x))  \
+\       ((? x. S x) --> (! x. L x --> M x))  \
 \   --> (! x. P x & L x --> M x)";
 by (safe_meson_tac 1);  
 result();
@@ -361,7 +361,7 @@
 result();
 
 writeln"Problem 31";  (*10 Horn clauses; first negative clauses is useless*)
-goal HOL.thy "~(? x.P x & (Q x | R x)) & \
+goal HOL.thy "~(? x. P x & (Q x | R x)) & \
 \       (? x. L x & P x) & \
 \       (! x. ~ R x --> M x)  \
 \   --> (? x. L x & M x)";
@@ -407,7 +407,7 @@
 
 writeln"Problem 37";  (*10 Horn clauses*)
 goal HOL.thy "(! z. ? w. ! x. ? y. \
-\          (P x z --> P y w) & P y z & (P y w --> (? u.Q u w))) & \
+\          (P x z --> P y w) & P y z & (P y w --> (? u. Q u w))) & \
 \       (! x z. ~P x z --> (? y. Q y z)) & \
 \       ((? x y. Q x y) --> (! x. R x x))  \
 \   --> (! x. ? y. R x y)";
@@ -475,7 +475,7 @@
 writeln"Problem 46";  (*26 Horn clauses; 21-step proof*)
 goal HOL.thy
     "(! x. f x & (! y. f y & h y x --> g y) --> g x) &      \
-\    ((? x.f x & ~g x) -->                                    \
+\    ((? x. f x & ~g x) -->                                    \
 \     (? x. f x & ~g x & (! y. f y & ~g y --> j x y))) &    \
 \    (! x y. f x & f y & h x y --> ~j y x)                    \
 \     --> (! x. f x --> g x)";
@@ -486,22 +486,22 @@
 writeln"Problem 47.  Schubert's Steamroller";
         (*26 clauses; 63 Horn clauses*)
 goal HOL.thy
-    "(! x. P1 x --> P0 x) & (? x.P1 x) &     \
-\    (! x. P2 x --> P0 x) & (? x.P2 x) &     \
-\    (! x. P3 x --> P0 x) & (? x.P3 x) &     \
-\    (! x. P4 x --> P0 x) & (? x.P4 x) &     \
-\    (! x. P5 x --> P0 x) & (? x.P5 x) &     \
-\    (! x. Q1 x --> Q0 x) & (? x.Q1 x) &     \
-\    (! x. P0 x --> ((! y.Q0 y-->R x y) |    \
-\                     (! y.P0 y & S y x &     \
-\                          (? z.Q0 z&R y z) --> R x y))) &   \
+    "(! x. P1 x --> P0 x) & (? x. P1 x) &     \
+\    (! x. P2 x --> P0 x) & (? x. P2 x) &     \
+\    (! x. P3 x --> P0 x) & (? x. P3 x) &     \
+\    (! x. P4 x --> P0 x) & (? x. P4 x) &     \
+\    (! x. P5 x --> P0 x) & (? x. P5 x) &     \
+\    (! x. Q1 x --> Q0 x) & (? x. Q1 x) &     \
+\    (! x. P0 x --> ((! y. Q0 y-->R x y) |    \
+\                     (! y. P0 y & S y x &     \
+\                          (? z. Q0 z&R y z) --> R x y))) &   \
 \    (! x y. P3 y & (P5 x|P4 x) --> S x y) &        \
 \    (! x y. P3 x & P2 y --> S x y) &        \
 \    (! x y. P2 x & P1 y --> S x y) &        \
 \    (! x y. P1 x & (P2 y|Q1 y) --> ~R x y) &       \
 \    (! x y. P3 x & P4 y --> R x y) &        \
 \    (! x y. P3 x & P5 y --> ~R x y) &       \
-\    (! x. (P4 x|P5 x) --> (? y.Q0 y & R x y))      \
+\    (! x. (P4 x|P5 x) --> (? y. Q0 y & R x y))      \
 \    --> (? x y. P0 x & P0 y & (? z. Q1 z & R y z & R x y))";
 by (safe_meson_tac 1);   (*119 secs*)
 result();
@@ -518,14 +518,14 @@
 (*A similar example, suggested by Johannes Schumann and credited to Pelletier*)
 goal HOL.thy "(!x y z. P x y --> P y z --> P x z) --> \
 \       (!x y z. Q x y --> Q y z --> Q x z) --> \
-\       (!x y.Q x y --> Q y x) -->  (!x y. P x y | Q x y) --> \
-\       (!x y.P x y) | (!x y.Q x y)";
+\       (!x y. Q x y --> Q y x) -->  (!x y. P x y | Q x y) --> \
+\       (!x y. P x y) | (!x y. Q x y)";
 by (safe_best_meson_tac 1);          (*2.7 secs*)
 result();
 
 writeln"Problem 50";  
 (*What has this to do with equality?*)
-goal HOL.thy "(! x. P a x | (! y.P x y)) --> (? x. ! y.P x y)";
+goal HOL.thy "(! x. P a x | (! y. P x y)) --> (? x. ! y. P x y)";
 by (safe_meson_tac 1);
 result();
 
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/ex/set.ML
--- a/src/HOL/ex/set.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/ex/set.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -21,7 +21,7 @@
 
 (*** A unique fixpoint theorem --- fast/best/meson all fail ***)
 
-val [prem] = goal HOL.thy "?!x.f(g(x))=x ==> ?!y.g(f(y))=y";
+val [prem] = goal HOL.thy "?!x. f(g(x))=x ==> ?!y. g(f(y))=y";
 by (EVERY1[rtac (prem RS ex1E), rtac ex1I, etac arg_cong,
           rtac subst, atac, etac allE, rtac arg_cong, etac mp, etac arg_cong]);
 result();
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/mono.ML
--- a/src/HOL/mono.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/mono.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -91,12 +91,12 @@
 qed "imp_refl";
 
 val [PQimp] = goal HOL.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 (blast_tac (!claset addIs [PQimp RS mp]) 1);
 qed "ex_mono";
 
 val [PQimp] = goal HOL.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 (blast_tac (!claset addIs [PQimp RS mp]) 1);
 qed "all_mono";
 
diff -r 22bbc1676768 -r b55686a7b22c src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOL/simpdata.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -102,7 +102,7 @@
    "(P | False) = P", "(False | P) = P",
    "(P | P) = P", "(P | (P | Q)) = (P | Q)",
    "((~P) = (~Q)) = (P=Q)",
-   "(!x.P) = P", "(? x.P) = P", "? x. x=t", "? x. t=x", 
+   "(!x. P) = P", "(? x. P) = P", "? x. x=t", "? x. t=x", 
    "(? x. x=t & P(x)) = P(t)",
    "(! x. t=x --> P(x)) = P(t)" ];
 
@@ -122,21 +122,21 @@
 
 (*Miniscoping: pushing in existential quantifiers*)
 val ex_simps = map prover 
-                ["(EX x. P x & Q)   = ((EX x.P x) & Q)",
-                 "(EX x. P & Q x)   = (P & (EX x.Q x))",
-                 "(EX x. P x | Q)   = ((EX x.P x) | Q)",
-                 "(EX x. P | Q x)   = (P | (EX x.Q x))",
-                 "(EX x. P x --> Q) = ((ALL x.P x) --> Q)",
-                 "(EX x. P --> Q x) = (P --> (EX x.Q x))"];
+                ["(EX x. P x & Q)   = ((EX x. P x) & Q)",
+                 "(EX x. P & Q x)   = (P & (EX x. Q x))",
+                 "(EX x. P x | Q)   = ((EX x. P x) | Q)",
+                 "(EX x. P | Q x)   = (P | (EX x. Q x))",
+                 "(EX x. P x --> Q) = ((ALL x. P x) --> Q)",
+                 "(EX x. P --> Q x) = (P --> (EX x. Q x))"];
 
 (*Miniscoping: pushing in universal quantifiers*)
 val all_simps = map prover
-                ["(ALL x. P x & Q)   = ((ALL x.P x) & Q)",
-                 "(ALL x. P & Q x)   = (P & (ALL x.Q x))",
-                 "(ALL x. P x | Q)   = ((ALL x.P x) | Q)",
-                 "(ALL x. P | Q x)   = (P | (ALL x.Q x))",
-                 "(ALL x. P x --> Q) = ((EX x.P x) --> Q)",
-                 "(ALL x. P --> Q x) = (P --> (ALL x.Q x))"];
+                ["(ALL x. P x & Q)   = ((ALL x. P x) & Q)",
+                 "(ALL x. P & Q x)   = (P & (ALL x. Q x))",
+                 "(ALL x. P x | Q)   = ((ALL x. P x) | Q)",
+                 "(ALL x. P | Q x)   = (P | (ALL x. Q x))",
+                 "(ALL x. P x --> Q) = ((EX x. P x) --> Q)",
+                 "(ALL x. P --> Q x) = (P --> (ALL x. Q x))"];
 
 (*** Simplification procedure for turning  ? x. ... & x = t & ...
      into                                  ? x. x = t & ... & ...
@@ -179,7 +179,7 @@
           in Some(prove_eq ceqt) end)
   | rearrange _ _ _ = None;
 
-val pattern = read_cterm (sign_of HOL.thy) ("? x.P(x) & Q(x)",HOLogic.boolT)
+val pattern = read_cterm (sign_of HOL.thy) ("? x. P(x) & Q(x)",HOLogic.boolT)
 
 in
 val defEX_regroup = mk_simproc "defined EX" [pattern] rearrange;
@@ -242,9 +242,9 @@
   cases boil down to the same thing.*) 
 prove "cases_simp" "((P --> Q) & (~P --> Q)) = Q";
 
-prove "not_all" "(~ (! x.P(x))) = (? x.~P(x))";
+prove "not_all" "(~ (! x. P(x))) = (? x.~P(x))";
 prove "imp_all" "((! x. P x) --> Q) = (? x. P x --> Q)";
-prove "not_ex"  "(~ (? x.P(x))) = (! x.~P(x))";
+prove "not_ex"  "(~ (? x. P(x))) = (! x.~P(x))";
 prove "imp_ex" "((? x. P x) --> Q) = (! x. P x --> Q)";
 
 prove "ex_disj_distrib" "(? x. P(x) | Q(x)) = ((? x. P(x)) | (? x. Q(x)))";
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/Cfun2.ML
--- a/src/HOLCF/Cfun2.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Cfun2.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -9,7 +9,7 @@
 open Cfun2;
 
 (* for compatibility with old HOLCF-Version *)
-qed_goal "inst_cfun_po" thy "(op <<)=(%f1 f2.fapp f1 << fapp f2)"
+qed_goal "inst_cfun_po" thy "(op <<)=(%f1 f2. fapp f1 << fapp f2)"
  (fn prems => 
         [
 	(fold_goals_tac [less_cfun_def]),
@@ -30,7 +30,7 @@
 (* Type 'a ->'b  is pointed                                                 *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goal "minimal_cfun" thy "fabs(% x.UU) << f"
+qed_goal "minimal_cfun" thy "fabs(% x. UU) << f"
 (fn prems =>
         [
         (stac less_cfun 1),
@@ -41,10 +41,10 @@
 
 bind_thm ("UU_cfun_def",minimal_cfun RS minimal2UU RS sym);
 
-qed_goal "least_cfun" thy "? x::'a->'b::pcpo.!y.x<<y"
+qed_goal "least_cfun" thy "? x::'a->'b::pcpo.!y. x<<y"
 (fn prems =>
         [
-        (res_inst_tac [("x","fabs(% x.UU)")] exI 1),
+        (res_inst_tac [("x","fabs(% x. UU)")] exI 1),
         (rtac (minimal_cfun RS allI) 1)
         ]);
 
@@ -156,7 +156,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "lub_cfun_mono" thy 
-        "is_chain(F) ==> monofun(% x.lub(range(% j.(F j)`x)))"
+        "is_chain(F) ==> monofun(% x. lub(range(% j.(F j)`x)))"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -190,7 +190,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "cont_lubcfun" thy 
-        "is_chain(F) ==> cont(% x.lub(range(% j.F(j)`x)))"
+        "is_chain(F) ==> cont(% x. lub(range(% j. F(j)`x)))"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -209,7 +209,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "lub_cfun" thy 
-  "is_chain(CCF) ==> range(CCF) <<| (LAM x.lub(range(% i.CCF(i)`x)))"
+  "is_chain(CCF) ==> range(CCF) <<| (LAM x. lub(range(% i. CCF(i)`x)))"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/Cfun3.ML
--- a/src/HOLCF/Cfun3.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Cfun3.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -7,7 +7,7 @@
 open Cfun3;
 
 (* for compatibility with old HOLCF-Version *)
-qed_goal "inst_cfun_pcpo" thy "UU = fabs(%x.UU)"
+qed_goal "inst_cfun_pcpo" thy "UU = fabs(%x. UU)"
  (fn prems => 
         [
         (simp_tac (HOL_ss addsimps [UU_def,UU_cfun_def]) 1)
@@ -53,7 +53,7 @@
 
 qed_goal "contlub_cfun_fun" thy 
 "is_chain(FY) ==>\
-\ lub(range FY)`x = lub(range (%i.FY(i)`x))"
+\ lub(range FY)`x = lub(range (%i. FY(i)`x))"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -67,7 +67,7 @@
 
 qed_goal "cont_cfun_fun" thy 
 "is_chain(FY) ==>\
-\ range(%i.FY(i)`x) <<| lub(range FY)`x"
+\ range(%i. FY(i)`x) <<| lub(range FY)`x"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -83,7 +83,7 @@
 
 qed_goal "contlub_cfun" thy 
 "[|is_chain(FY);is_chain(TY)|] ==>\
-\ (lub(range FY))`(lub(range TY)) = lub(range(%i.FY(i)`(TY i)))"
+\ (lub(range FY))`(lub(range TY)) = lub(range(%i. FY(i)`(TY i)))"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -117,7 +117,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "cont2cont_fapp" thy 
-        "[|cont(%x.ft x);cont(%x.tt x)|] ==> cont(%x. (ft x)`(tt x))"
+        "[|cont(%x. ft x);cont(%x. tt x)|] ==> cont(%x. (ft x)`(tt x))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -137,7 +137,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "cont2mono_LAM" thy 
- "[| !!x.cont(c1 x); !!y.monofun(%x.c1 x y)|] ==> monofun(%x. LAM y. c1 x y)"
+ "[| !!x. cont(c1 x); !!y. monofun(%x. c1 x y)|] ==> monofun(%x. LAM y. c1 x y)"
 (fn [p1,p2] =>
         [
         (rtac monofunI 1),
@@ -157,7 +157,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "cont2cont_LAM" thy 
- "[| !!x.cont(c1 x); !!y.cont(%x.c1 x y) |] ==> cont(%x. LAM y. c1 x y)"
+ "[| !!x. cont(c1 x); !!y. cont(%x. c1 x y) |] ==> cont(%x. LAM y. c1 x y)"
 (fn [p1,p2] =>
         [
         (rtac monocontlub2cont 1),
@@ -393,7 +393,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "iso_strict"  thy  
-"!!f g.[|!y.f`(g`y)=(y::'b) ; !x.g`(f`x)=(x::'a) |] \
+"!!f g.[|!y. f`(g`y)=(y::'b) ; !x. g`(f`x)=(x::'a) |] \
 \ ==> f`UU=UU & g`UU=UU"
  (fn prems =>
         [
@@ -410,7 +410,7 @@
 
 
 qed_goal "isorep_defined" thy 
-        "[|!x.rep`(abs`x)=x;!y.abs`(rep`y)=y; z~=UU|] ==> rep`z ~= UU"
+        "[|!x. rep`(abs`x)=x;!y. abs`(rep`y)=y; z~=UU|] ==> rep`z ~= UU"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -424,7 +424,7 @@
         ]);
 
 qed_goal "isoabs_defined" thy 
-        "[|!x.rep`(abs`x) = x;!y.abs`(rep`y)=y ; z~=UU|] ==> abs`z ~= UU"
+        "[|!x. rep`(abs`x) = x;!y. abs`(rep`y)=y ; z~=UU|] ==> abs`z ~= UU"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -442,14 +442,14 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "chfin2chfin" thy "!!f g.[|! Y::nat=>'a. is_chain Y --> (? n. max_in_chain n Y); \
-\ !y.f`(g`y)=(y::'b) ; !x.g`(f`x)=(x::'a::chfin) |] \
+\ !y. f`(g`y)=(y::'b) ; !x. g`(f`x)=(x::'a::chfin) |] \
 \ ==> ! Y::nat=>'b. is_chain Y --> (? n. max_in_chain n Y)"
  (fn prems =>
         [
         (rewtac max_in_chain_def),
         (strip_tac 1),
         (rtac exE 1),
-        (res_inst_tac [("P","is_chain(%i.g`(Y i))")] mp 1),
+        (res_inst_tac [("P","is_chain(%i. g`(Y i))")] mp 1),
         (etac spec 1),
         (etac ch2ch_fappR 1),
         (rtac exI 1),
@@ -465,8 +465,8 @@
         ]);
 
 
-qed_goal "flat2flat" thy "!!f g.[|!x y::'a.x<<y --> x=UU | x=y; \
-\ !y.f`(g`y)=(y::'b); !x.g`(f`x)=(x::'a)|] ==> !x y::'b.x<<y --> x=UU | x=y"
+qed_goal "flat2flat" thy "!!f g.[|!x y::'a. x<<y --> x=UU | x=y; \
+\ !y. f`(g`y)=(y::'b); !x. g`(f`x)=(x::'a)|] ==> !x y::'b. x<<y --> x=UU | x=y"
  (fn prems =>
         [
         (strip_tac 1),
@@ -496,7 +496,7 @@
 (* ------------------------------------------------------------------------- *)
 
 qed_goal "flat_codom" thy 
-"f`(x::'a)=(c::'b::flat) ==> f`(UU::'a)=(UU::'b) | (!z.f`(z::'a)=c)"
+"f`(x::'a)=(c::'b::flat) ==> f`(UU::'a)=(UU::'b) | (!z. f`(z::'a)=c)"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -534,7 +534,7 @@
         (rtac refl 1)
         ]);
 
-qed_goalw "cfcomp1" thy [oo_def] "(f oo g)=(LAM x.f`(g`x))" (fn _ => [
+qed_goalw "cfcomp1" thy [oo_def] "(f oo g)=(LAM x. f`(g`x))" (fn _ => [
         (stac beta_cfun 1),
         (Simp_tac 1),
         (stac beta_cfun 1),
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/Cfun3.thy
--- a/src/HOLCF/Cfun3.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Cfun3.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -20,7 +20,7 @@
 defs
 
 Istrictify_def  "Istrictify f x == if x=UU then UU else f`x"    
-strictify_def   "strictify == (LAM f x.Istrictify f x)"
+strictify_def   "strictify == (LAM f x. Istrictify f x)"
 
 consts
         ID      :: "('a::cpo) -> 'a"
@@ -32,7 +32,7 @@
 
 defs
 
-  ID_def        "ID ==(LAM x.x)"
-  oo_def        "cfcomp == (LAM f g x.f`(g`x))" 
+  ID_def        "ID ==(LAM x. x)"
+  oo_def        "cfcomp == (LAM f g x. f`(g`x))" 
 
 end
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/Cont.ML
--- a/src/HOLCF/Cont.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Cont.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -32,7 +32,7 @@
 
 
 qed_goalw "contI" thy [cont]
- "! Y. is_chain(Y) --> range(% i.f(Y(i))) <<| f(lub(range(Y))) ==> cont(f)"
+ "! Y. is_chain(Y) --> range(% i. f(Y(i))) <<| f(lub(range(Y))) ==> cont(f)"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -40,7 +40,7 @@
         ]);
 
 qed_goalw "contE" thy [cont]
- "cont(f) ==> ! Y. is_chain(Y) --> range(% i.f(Y(i))) <<| f(lub(range(Y)))"
+ "cont(f) ==> ! Y. is_chain(Y) --> range(% i. f(Y(i))) <<| f(lub(range(Y)))"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -89,7 +89,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "ub2ub_monofun" thy 
- "[| monofun(f); range(Y) <| u|]  ==> range(%i.f(Y(i))) <| f(u)"
+ "[| monofun(f); range(Y) <| u|]  ==> range(%i. f(Y(i))) <| f(u)"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -213,7 +213,7 @@
         ]);
 
 qed_goal "ch2ch_MF2LR" thy 
-"[|monofun(MF2); !f.monofun(MF2(f)); is_chain(F); is_chain(Y)|] ==> \
+"[|monofun(MF2); !f. monofun(MF2(f)); is_chain(F); is_chain(Y)|] ==> \
 \  is_chain(%i. MF2(F(i))(Y(i)))"
  (fn prems =>
         [
@@ -230,7 +230,7 @@
 
 qed_goal "ch2ch_lubMF2R" thy 
 "[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
-\  !f.monofun(MF2(f)::('b::po=>'c::cpo));\
+\  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
 \       is_chain(F);is_chain(Y)|] ==> \
 \       is_chain(%j. lub(range(%i. MF2 (F j) (Y i))))"
 (fn prems =>
@@ -250,7 +250,7 @@
 
 qed_goal "ch2ch_lubMF2L" thy 
 "[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
-\  !f.monofun(MF2(f)::('b::po=>'c::cpo));\
+\  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
 \       is_chain(F);is_chain(Y)|] ==> \
 \       is_chain(%i. lub(range(%j. MF2 (F j) (Y i))))"
 (fn prems =>
@@ -270,9 +270,9 @@
 
 qed_goal "lub_MF2_mono" thy 
 "[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
-\  !f.monofun(MF2(f)::('b::po=>'c::cpo));\
+\  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
 \       is_chain(F)|] ==> \
-\       monofun(% x.lub(range(% j.MF2 (F j) (x))))"
+\       monofun(% x. lub(range(% j. MF2 (F j) (x))))"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -290,7 +290,7 @@
 
 qed_goal "ex_lubMF2" thy 
 "[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
-\  !f.monofun(MF2(f)::('b::po=>'c::cpo));\
+\  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
 \       is_chain(F); is_chain(Y)|] ==> \
 \               lub(range(%j. lub(range(%i. MF2(F j) (Y i))))) =\
 \               lub(range(%i. lub(range(%j. MF2(F j) (Y i)))))"
@@ -329,7 +329,7 @@
 
 qed_goal "diag_lubMF2_1" thy 
 "[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
-\  !f.monofun(MF2(f)::('b::po=>'c::cpo));\
+\  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
 \  is_chain(FY);is_chain(TY)|] ==>\
 \ lub(range(%i. lub(range(%j. MF2(FY(j))(TY(i)))))) =\
 \ lub(range(%i. MF2(FY(i))(TY(i))))"
@@ -373,7 +373,7 @@
 
 qed_goal "diag_lubMF2_2" thy 
 "[|monofun(MF2::('a::po=>'b::po=>'c::cpo));\
-\  !f.monofun(MF2(f)::('b::po=>'c::cpo));\
+\  !f. monofun(MF2(f)::('b::po=>'c::cpo));\
 \  is_chain(FY);is_chain(TY)|] ==>\
 \ lub(range(%j. lub(range(%i. MF2(FY(j))(TY(i)))))) =\
 \ lub(range(%i. MF2(FY(i))(TY(i))))"
@@ -394,8 +394,8 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "contlub_CF2" thy 
-"[|cont(CF2);!f.cont(CF2(f));is_chain(FY);is_chain(TY)|] ==>\
-\ CF2(lub(range(FY)))(lub(range(TY))) = lub(range(%i.CF2(FY(i))(TY(i))))"
+"[|cont(CF2);!f. cont(CF2(f));is_chain(FY);is_chain(TY)|] ==>\
+\ CF2(lub(range(FY)))(lub(range(TY))) = lub(range(%i. CF2(FY(i))(TY(i))))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -486,7 +486,7 @@
 (*********  Note "(%x.%y.c1 x y) = c1" ***********)
 
 qed_goal "mono2mono_MF1L_rev" thy
-        "!y.monofun(%x.c1 x y) ==> monofun(c1)"
+        "!y. monofun(%x. c1 x y) ==> monofun(c1)"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -499,7 +499,7 @@
         ]);
 
 qed_goal "cont2cont_CF1L_rev" thy
-        "!y.cont(%x.c1 x y) ==> cont(c1)"
+        "!y. cont(%x. c1 x y) ==> cont(c1)"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -524,8 +524,8 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "contlub_abstraction" thy
-"[|is_chain(Y::nat=>'a);!y.cont(%x.(c::'a::cpo=>'b::cpo=>'c::cpo) x y)|] ==>\
-\ (%y.lub(range(%i.c (Y i) y))) = (lub(range(%i.%y.c (Y i) y)))"
+"[|is_chain(Y::nat=>'a);!y. cont(%x.(c::'a::cpo=>'b::cpo=>'c::cpo) x y)|] ==>\
+\ (%y. lub(range(%i. c (Y i) y))) = (lub(range(%i.%y. c (Y i) y)))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -540,7 +540,7 @@
         ]);
 
 qed_goal "mono2mono_app" thy 
-"[|monofun(ft);!x.monofun(ft(x));monofun(tt)|] ==>\
+"[|monofun(ft);!x. monofun(ft(x));monofun(tt)|] ==>\
 \        monofun(%x.(ft(x))(tt(x)))"
  (fn prems =>
         [
@@ -558,7 +558,7 @@
 
 
 qed_goal "cont2contlub_app" thy 
-"[|cont(ft);!x.cont(ft(x));cont(tt)|] ==> contlub(%x.(ft(x))(tt(x)))"
+"[|cont(ft);!x. cont(ft(x));cont(tt)|] ==> contlub(%x.(ft(x))(tt(x)))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -575,7 +575,7 @@
 
 
 qed_goal "cont2cont_app" thy 
-"[|cont(ft);!x.cont(ft(x));cont(tt)|] ==>\
+"[|cont(ft);!x. cont(ft(x));cont(tt)|] ==>\
 \        cont(%x.(ft(x))(tt(x)))"
  (fn prems =>
         [
@@ -605,7 +605,7 @@
 (* The identity function is continuous                                      *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goal "cont_id" thy "cont(% x.x)"
+qed_goal "cont_id" thy "cont(% x. x)"
  (fn prems =>
         [
         (rtac contI 1),
@@ -618,7 +618,7 @@
 (* constant functions are continuous                                        *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goalw "cont_const" thy [cont] "cont(%x.c)"
+qed_goalw "cont_const" thy [cont] "cont(%x. c)"
  (fn prems =>
         [
         (strip_tac 1),
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/Cont.thy
--- a/src/HOLCF/Cont.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Cont.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -28,10 +28,10 @@
 monofun         "monofun(f) == ! x y. x << y --> f(x) << f(y)"
 
 contlub         "contlub(f) == ! Y. is_chain(Y) --> 
-                                f(lub(range(Y))) = lub(range(% i.f(Y(i))))"
+                                f(lub(range(Y))) = lub(range(% i. f(Y(i))))"
 
 cont            "cont(f)   == ! Y. is_chain(Y) --> 
-                                range(% i.f(Y(i))) <<| f(lub(range(Y)))"
+                                range(% i. f(Y(i))) <<| f(lub(range(Y)))"
 
 (* ------------------------------------------------------------------------ *)
 (* the main purpose of cont.thy is to show:                                 *)
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/Cprod2.ML
--- a/src/HOLCF/Cprod2.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Cprod2.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -9,7 +9,7 @@
 open Cprod2;
 
 (* for compatibility with old HOLCF-Version *)
-qed_goal "inst_cprod_po" thy "(op <<)=(%x y.fst x<<fst y & snd x<<snd y)"
+qed_goal "inst_cprod_po" thy "(op <<)=(%x y. fst x<<fst y & snd x<<snd y)"
  (fn prems => 
         [
         (fold_goals_tac [less_cprod_def]),
@@ -45,7 +45,7 @@
 
 bind_thm ("UU_cprod_def",minimal_cprod RS minimal2UU RS sym);
 
-qed_goal "least_cprod" thy "? x::'a*'b.!y.x<<y"
+qed_goal "least_cprod" thy "? x::'a*'b.!y. x<<y"
 (fn prems =>
         [
         (res_inst_tac [("x","(UU,UU)")] exI 1),
@@ -116,7 +116,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "lub_cprod" thy 
-"is_chain S ==> range S<<|(lub(range(%i.fst(S i))),lub(range(%i.snd(S i))))"
+"is_chain S ==> range S<<|(lub(range(%i. fst(S i))),lub(range(%i. snd(S i))))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -147,7 +147,7 @@
 
 *)
 
-qed_goal "cpo_cprod" thy "is_chain(S::nat=>'a::cpo*'b::cpo)==>? x.range S<<| x"
+qed_goal "cpo_cprod" thy "is_chain(S::nat=>'a::cpo*'b::cpo)==>? x. range S<<| x"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/Cprod3.ML
--- a/src/HOLCF/Cprod3.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Cprod3.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -262,7 +262,7 @@
 
 qed_goalw "lub_cprod2" Cprod3.thy [cfst_def,csnd_def,cpair_def]
 "[|is_chain(S)|] ==> range(S) <<| \
-\ <(lub(range(%i.cfst`(S i)))) , lub(range(%i.csnd`(S i)))>"
+\ <(lub(range(%i. cfst`(S i)))) , lub(range(%i. csnd`(S i)))>"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/Cprod3.thy
--- a/src/HOLCF/Cprod3.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Cprod3.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -26,9 +26,9 @@
 
 defs
 cpair_def       "cpair  == (LAM x y.(x,y))"
-cfst_def        "cfst   == (LAM p.fst(p))"
-csnd_def        "csnd   == (LAM p.snd(p))"      
-csplit_def      "csplit == (LAM f p.f`(cfst`p)`(csnd`p))"
+cfst_def        "cfst   == (LAM p. fst(p))"
+csnd_def        "csnd   == (LAM p. snd(p))"      
+csplit_def      "csplit == (LAM f p. f`(cfst`p)`(csnd`p))"
 
 
 
@@ -43,7 +43,7 @@
 
 constdefs
   CLet           :: "'a -> ('a -> 'b) -> 'b"
-  "CLet == LAM s f.f`s"
+  "CLet == LAM s f. f`s"
 
 
 (* syntax for Let *)
@@ -59,7 +59,7 @@
 
 translations
   "_CLet (_Cbinds b bs) e"  == "_CLet b (_CLet bs e)"
-  "Let x = a in e"          == "CLet`a`(LAM x.e)"
+  "Let x = a in e"          == "CLet`a`(LAM x. e)"
 
 
 (* syntax for LAM <x,y,z>.e *)
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/Discrete.ML
--- a/src/HOLCF/Discrete.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Discrete.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -10,11 +10,11 @@
 Addsimps [undiscr_Discr];
 
 goal thy
- "!!S::nat=>('a::term)discr. is_chain(S) ==> range(%i.f(S i)) = {f(S 0)}";
+ "!!S::nat=>('a::term)discr. is_chain(S) ==> range(%i. f(S i)) = {f(S 0)}";
 by(fast_tac (!claset addDs [discr_chain0] addEs [arg_cong]) 1);
 qed "discr_chain_f_range0";
 
-goalw thy [cont,is_lub,is_ub] "cont(%x::('a::term)discr.f x)";
+goalw thy [cont,is_lub,is_ub] "cont(%x::('a::term)discr. f x)";
 by(simp_tac (!simpset addsimps [discr_chain_f_range0]) 1);
 qed "cont_discr";
 AddIffs [cont_discr];
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/Fix.ML
--- a/src/HOLCF/Fix.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Fix.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -43,7 +43,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goalw "is_chain_iterate2" thy [is_chain] 
-        " x << F`x ==> is_chain (%i.iterate i F x)"
+        " x << F`x ==> is_chain (%i. iterate i F x)"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -57,7 +57,7 @@
 
 
 qed_goal "is_chain_iterate" thy  
-        "is_chain (%i.iterate i F UU)"
+        "is_chain (%i. iterate i F UU)"
  (fn prems =>
         [
         (rtac is_chain_iterate2 1),
@@ -452,16 +452,16 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goalw "admI" thy [adm_def]
-        "(!!Y. [| is_chain(Y); !i.P(Y(i)) |] ==> P(lub(range(Y)))) ==> adm(P)"
+        "(!!Y. [| is_chain(Y); !i. P(Y(i)) |] ==> P(lub(range(Y)))) ==> adm(P)"
  (fn prems => [fast_tac (HOL_cs addIs prems) 1]);
 
 qed_goalw "admD" thy [adm_def]
-        "!!P. [| adm(P); is_chain(Y); !i.P(Y(i)) |] ==> P(lub(range(Y)))"
+        "!!P. [| adm(P); is_chain(Y); !i. P(Y(i)) |] ==> P(lub(range(Y)))"
  (fn prems => [fast_tac HOL_cs 1]);
 
 qed_goalw "admw_def2" thy [admw_def]
-        "admw(P) = (!F.(!n.P(iterate n F UU)) -->\
-\                        P (lub(range(%i.iterate i F UU))))"
+        "admw(P) = (!F.(!n. P(iterate n F UU)) -->\
+\                        P (lub(range(%i. iterate i F UU))))"
  (fn prems =>
         [
         (rtac refl 1)
@@ -537,7 +537,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goalw "adm_max_in_chain"  thy  [adm_def]
-"!Y. is_chain(Y::nat=>'a) --> (? n.max_in_chain n Y) ==> adm(P::'a=>bool)"
+"!Y. is_chain(Y::nat=>'a) --> (? n. max_in_chain n Y) ==> adm(P::'a=>bool)"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -585,7 +585,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goalw "adm_less"  thy [adm_def]
-        "[|cont u;cont v|]==> adm(%x.u x << v x)"
+        "[|cont u;cont v|]==> adm(%x. u x << v x)"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -610,7 +610,7 @@
  (fn prems => [fast_tac (HOL_cs addEs [admD] addIs [admI]) 1]);
 Addsimps [adm_conj];
 
-qed_goalw "adm_not_free"  thy [adm_def] "adm(%x.t)"
+qed_goalw "adm_not_free"  thy [adm_def] "adm(%x. t)"
  (fn prems => [fast_tac HOL_cs 1]);
 Addsimps [adm_not_free];
 
@@ -629,7 +629,7 @@
         ]);
 
 qed_goal "adm_all" thy  
-        "!!P. !y.adm(P y) ==> adm(%x.!y.P y x)"
+        "!!P. !y. adm(P y) ==> adm(%x.!y. P y x)"
  (fn prems => [fast_tac (HOL_cs addIs [admI] addEs [admD]) 1]);
 
 bind_thm ("adm_all2", allI RS adm_all);
@@ -681,7 +681,7 @@
 local
 
   val adm_disj_lemma1 = prove_goal HOL.thy 
-  "!n.P(Y n)|Q(Y n) ==> (? i.!j.R i j --> Q(Y(j))) | (!i.? j.R i j & P(Y(j)))"
+  "!n. P(Y n)|Q(Y n) ==> (? i.!j. R i j --> Q(Y(j))) | (!i.? j. R i j & P(Y(j)))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -689,7 +689,7 @@
         ]);
 
   val adm_disj_lemma2 = prove_goal thy  
-  "!!Q. [| adm(Q); ? X.is_chain(X) & (!n.Q(X(n))) &\
+  "!!Q. [| adm(Q); ? X. is_chain(X) & (!n. Q(X(n))) &\
   \   lub(range(Y))=lub(range(X))|] ==> Q(lub(range(Y)))"
  (fn _ => [fast_tac (!claset addEs [admD] addss !simpset) 1]);
 
@@ -735,7 +735,7 @@
         [
         (cut_facts_tac prems 1),
         (etac exE 1),
-        (res_inst_tac [("x","%m.if m<Suc(i) then Y(Suc(i)) else Y m")] exI 1),
+        (res_inst_tac [("x","%m. if m<Suc(i) then Y(Suc(i)) else Y m")] exI 1),
         (rtac conjI 1),
         (rtac adm_disj_lemma3 1),
         (atac 1),
@@ -854,7 +854,7 @@
         ]);
 
 val adm_disj = prove_goal thy  
-        "!!P. [| adm P; adm Q |] ==> adm(%x.P x | Q x)"
+        "!!P. [| adm P; adm Q |] ==> adm(%x. P x | Q x)"
  (fn prems =>
         [
         (rtac admI 1),
@@ -876,10 +876,10 @@
 bind_thm("adm_disj",adm_disj);
 
 qed_goal "adm_imp"  thy  
-        "!!P. [| adm(%x.~(P x)); adm Q |] ==> adm(%x.P x --> Q x)"
+        "!!P. [| adm(%x.~(P x)); adm Q |] ==> adm(%x. P x --> Q x)"
  (fn prems =>
         [
-        (subgoal_tac "(%x.P x --> Q x) = (%x. ~P x | Q x)" 1),
+        (subgoal_tac "(%x. P x --> Q x) = (%x. ~P x | Q x)" 1),
          (Asm_simp_tac 1),
          (etac adm_disj 1),
          (atac 1),
@@ -887,9 +887,9 @@
         (fast_tac HOL_cs 1)
         ]);
 
-goal Fix.thy "!! P. [| adm (%x. P x --> Q x); adm (%x.Q x --> P x) |] \
+goal Fix.thy "!! P. [| adm (%x. P x --> Q x); adm (%x. Q x --> P x) |] \
 \           ==> adm (%x. P x = Q x)";
-by(subgoal_tac "(%x.P x = Q x) = (%x. (P x --> Q x) & (Q x --> P x))" 1);
+by(subgoal_tac "(%x. P x = Q x) = (%x. (P x --> Q x) & (Q x --> P x))" 1);
 by (Asm_simp_tac 1);
 by (rtac ext 1);
 by (fast_tac HOL_cs 1);
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Fix.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -20,14 +20,14 @@
 
 defs
 
-iterate_def   "iterate n F c == nat_rec c (%n x.F`x) n"
-Ifix_def      "Ifix F == lub(range(%i.iterate i F UU))"
+iterate_def   "iterate n F c == nat_rec c (%n x. F`x) n"
+Ifix_def      "Ifix F == lub(range(%i. iterate i F UU))"
 fix_def       "fix == (LAM f. Ifix f)"
 
 adm_def       "adm P == !Y. is_chain(Y) --> 
-                        (!i.P(Y i)) --> P(lub(range Y))"
+                        (!i. P(Y i)) --> P(lub(range Y))"
 
-admw_def      "admw P == !F. (!n.P (iterate n F UU)) -->
+admw_def      "admw P == !F. (!n. P (iterate n F UU)) -->
                             P (lub(range (%i. iterate i F UU)))" 
 
 end
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/Fun2.ML
--- a/src/HOLCF/Fun2.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Fun2.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -9,7 +9,7 @@
 open Fun2;
 
 (* for compatibility with old HOLCF-Version *)
-qed_goal "inst_fun_po" thy "(op <<)=(%f g.!x.f x << g x)"
+qed_goal "inst_fun_po" thy "(op <<)=(%f g.!x. f x << g x)"
  (fn prems => 
         [
 	(fold_goals_tac [less_fun_def]),
@@ -20,7 +20,7 @@
 (* Type 'a::term => 'b::pcpo is pointed                                     *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goal "minimal_fun" thy "(%z.UU) << x"
+qed_goal "minimal_fun" thy "(%z. UU) << x"
 (fn prems =>
         [
         (simp_tac (!simpset addsimps [inst_fun_po,minimal]) 1)
@@ -28,10 +28,10 @@
 
 bind_thm ("UU_fun_def",minimal_fun RS minimal2UU RS sym);
 
-qed_goal "least_fun" thy "? x::'a=>'b::pcpo.!y.x<<y"
+qed_goal "least_fun" thy "? x::'a=>'b::pcpo.!y. x<<y"
 (fn prems =>
         [
-        (res_inst_tac [("x","(%z.UU)")] exI 1),
+        (res_inst_tac [("x","(%z. UU)")] exI 1),
         (rtac (minimal_fun RS allI) 1)
         ]);
 
@@ -52,7 +52,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "ch2ch_fun" thy 
-        "is_chain(S::nat=>('a=>'b::po)) ==> is_chain(% i.S(i)(x))"
+        "is_chain(S::nat=>('a=>'b::po)) ==> is_chain(% i. S(i)(x))"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -87,7 +87,7 @@
 
 qed_goal "lub_fun"  Fun2.thy
         "is_chain(S::nat=>('a::term => 'b::cpo)) ==> \
-\        range(S) <<| (% x.lub(range(% i.S(i)(x))))"
+\        range(S) <<| (% x. lub(range(% i. S(i)(x))))"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/Fun3.ML
--- a/src/HOLCF/Fun3.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Fun3.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -7,7 +7,7 @@
 open Fun3;
 
 (* for compatibility with old HOLCF-Version *)
-qed_goal "inst_fun_pcpo" thy "UU = (%x.UU)"
+qed_goal "inst_fun_pcpo" thy "UU = (%x. UU)"
  (fn prems => 
         [
         (simp_tac (HOL_ss addsimps [UU_def,UU_fun_def]) 1)
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/IMP/Denotational.thy
--- a/src/HOLCF/IMP/Denotational.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/IMP/Denotational.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -10,7 +10,7 @@
 
 constdefs
    dlift :: "(('a::term) discr -> 'b::pcpo) => ('a lift -> 'b)"
-  "dlift f == (LAM x.case x of Undef => UU | Def(y) => f`(Discr y))"
+  "dlift f == (LAM x. case x of Undef => UU | Def(y) => f`(Discr y))"
 
 consts D :: "com => state discr -> state lift"
 
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/IOA/ABP/Correctness.ML
--- a/src/HOLCF/IOA/ABP/Correctness.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/IOA/ABP/Correctness.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -6,7 +6,7 @@
 *)
 
 
-goal Abschannel.thy "(? x.x=P & Q(x)) = Q(P)";
+goal Abschannel.thy "(? x. x=P & Q(x)) = Q(P)";
 by (Fast_tac 1);
 qed"exis_elim";
 
@@ -209,7 +209,7 @@
 (* 3 thms that do not hold generally! The lucky restriction here is 
    the absence of internal actions. *)
 goal Correctness.thy 
-      "is_weak_ref_map (%id.id) sender_ioa sender_ioa";
+      "is_weak_ref_map (%id. id) sender_ioa sender_ioa";
 by (simp_tac (!simpset addsimps [is_weak_ref_map_def]) 1);
 by (TRY(
    (rtac conjI 1) THEN
@@ -225,7 +225,7 @@
 
 (* 2 copies of before *)
 goal Correctness.thy 
-      "is_weak_ref_map (%id.id) receiver_ioa receiver_ioa";
+      "is_weak_ref_map (%id. id) receiver_ioa receiver_ioa";
 by (simp_tac (!simpset addsimps [is_weak_ref_map_def]) 1);
 by (TRY(
    (rtac conjI 1) THEN
@@ -240,7 +240,7 @@
 qed"receiver_unchanged";
 
 goal Correctness.thy 
-      "is_weak_ref_map (%id.id) env_ioa env_ioa";
+      "is_weak_ref_map (%id. id) env_ioa env_ioa";
 by (simp_tac (!simpset addsimps [is_weak_ref_map_def]) 1);
 by (TRY(
    (rtac conjI 1) THEN
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/IOA/meta_theory/CompoExecs.ML
--- a/src/HOLCF/IOA/meta_theory/CompoExecs.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -193,7 +193,7 @@
 (* --------------------------------------------------------------------- *)
 
 goal thy "!s. (is_exec_frag (A||B) (s,xs) \
-\  --> Forall (%x.fst x:act (A||B)) xs)";
+\  --> Forall (%x. fst x:act (A||B)) xs)";
 
 by (pair_induct_tac "xs" [Forall_def,sforall_def,is_exec_frag_def] 1);
 (* main case *)
@@ -212,7 +212,7 @@
 \    is_exec_frag B (snd s,Filter_ex2 (asig_of B)`(ProjB2`xs)) &\
 \    stutter (asig_of A) (fst s,(ProjA2`xs)) & \
 \    stutter (asig_of B) (snd s,(ProjB2`xs)) & \
-\    Forall (%x.fst x:act (A||B)) xs \
+\    Forall (%x. fst x:act (A||B)) xs \
 \    --> is_exec_frag (A||B) (s,xs)";
 
 by (pair_induct_tac "xs" [Forall_def,sforall_def,
@@ -242,7 +242,7 @@
 \(Filter_ex (asig_of A) (ProjA ex) : executions A &\
 \ Filter_ex (asig_of B) (ProjB ex) : executions B &\
 \ stutter (asig_of A) (ProjA ex) & stutter (asig_of B) (ProjB ex) &\
-\ Forall (%x.fst x:act (A||B)) (snd ex))";
+\ Forall (%x. fst x:act (A||B)) (snd ex))";
 
 by (simp_tac (!simpset addsimps [executions_def,ProjB_def,
                                  Filter_ex_def,ProjA_def,starts_of_par]) 1);
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/IOA/meta_theory/CompoExecs.thy
--- a/src/HOLCF/IOA/meta_theory/CompoExecs.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -45,7 +45,7 @@
 
 
 Filter_ex2_def
-  "Filter_ex2 sig ==  Filter (%x.fst x:actions sig)"
+  "Filter_ex2 sig ==  Filter (%x. fst x:actions sig)"
 
 stutter_def
   "stutter sig ex == ((stutter2 sig`(snd ex)) (fst ex) ~= FF)"
@@ -70,7 +70,7 @@
         Int {ex. Filter_ex sigB (ProjB ex) : exB}
         Int {ex. stutter sigA (ProjA ex)}
         Int {ex. stutter sigB (ProjB ex)}
-        Int {ex. Forall (%x.fst x:(actions sigA Un actions sigB)) (snd ex)},
+        Int {ex. Forall (%x. fst x:(actions sigA Un actions sigB)) (snd ex)},
         asig_comp sigA sigB)"
 
 end
\ No newline at end of file
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/IOA/meta_theory/CompoScheds.ML
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -160,7 +160,7 @@
 
 goalw thy [filter_act_def,Filter_ex2_def]
    "filter_act`(Filter_ex2 (asig_of A)`xs)=\
-\   Filter (%a.a:act A)`(filter_act`xs)";
+\   Filter (%a. a:act A)`(filter_act`xs)";
 
 by (simp_tac (!simpset addsimps [MapFilter,o_def]) 1);
 qed"lemma_2_1a";
@@ -187,7 +187,7 @@
    is the same proposition, but we cannot change this one, when then rather lemma_1_1c  *)
 
 goal thy "!s. is_exec_frag (A||B) (s,xs) \
-\  --> Forall (%x.x:act (A||B)) (filter_act`xs)";
+\  --> Forall (%x. x:act (A||B)) (filter_act`xs)";
 
 by (pair_induct_tac "xs" [is_exec_frag_def,Forall_def,sforall_def] 1);
 (* main case *)
@@ -207,9 +207,9 @@
   --------------------------------------------------------------------------- *)
 
 goal thy "! exA exB s t. \
-\ Forall (%x.x:act (A||B)) sch  & \
-\ Filter (%a.a:act A)`sch << filter_act`exA &\
-\ Filter (%a.a:act B)`sch << filter_act`exB \
+\ Forall (%x. x:act (A||B)) sch  & \
+\ Filter (%a. a:act A)`sch << filter_act`exA &\
+\ Filter (%a. a:act B)`sch << filter_act`exB \
 \ --> filter_act`(snd (mkex A B sch (s,exA) (t,exB))) = sch";
 
 by (Seq_induct_tac "sch" [Filter_def,Forall_def,sforall_def,mkex_def] 1);
@@ -270,9 +270,9 @@
 
 
 goal thy "! exA exB s t. \
-\ Forall (%x.x:act (A||B)) sch & \
-\ Filter (%a.a:act A)`sch << filter_act`exA &\
-\ Filter (%a.a:act B)`sch << filter_act`exB \
+\ Forall (%x. x:act (A||B)) sch & \
+\ Filter (%a. a:act A)`sch << filter_act`exA &\
+\ Filter (%a. a:act B)`sch << filter_act`exB \
 \ --> stutter (asig_of A) (s,ProjA2`(snd (mkex A B sch (s,exA) (t,exB))))";
 
 by (mkex_induct_tac "sch" "exA" "exB");
@@ -281,9 +281,9 @@
 
 
 goal thy "!! sch.[|  \
-\ Forall (%x.x:act (A||B)) sch ; \
-\ Filter (%a.a:act A)`sch << filter_act`(snd exA) ;\
-\ Filter (%a.a:act B)`sch << filter_act`(snd exB) |] \
+\ Forall (%x. x:act (A||B)) sch ; \
+\ Filter (%a. a:act A)`sch << filter_act`(snd exA) ;\
+\ Filter (%a. a:act B)`sch << filter_act`(snd exB) |] \
 \ ==> stutter (asig_of A) (ProjA (mkex A B sch exA exB))";
 
 by (cut_facts_tac [stutterA_mkex] 1);
@@ -301,9 +301,9 @@
   --------------------------------------------------------------------------- *)
 
 goal thy "! exA exB s t. \
-\ Forall (%x.x:act (A||B)) sch & \
-\ Filter (%a.a:act A)`sch << filter_act`exA &\
-\ Filter (%a.a:act B)`sch << filter_act`exB \
+\ Forall (%x. x:act (A||B)) sch & \
+\ Filter (%a. a:act A)`sch << filter_act`exA &\
+\ Filter (%a. a:act B)`sch << filter_act`exB \
 \ --> stutter (asig_of B) (t,ProjB2`(snd (mkex A B sch (s,exA) (t,exB))))";
 
 by (mkex_induct_tac "sch" "exA" "exB");
@@ -312,9 +312,9 @@
 
 
 goal thy "!! sch.[|  \
-\ Forall (%x.x:act (A||B)) sch ; \
-\ Filter (%a.a:act A)`sch << filter_act`(snd exA) ;\
-\ Filter (%a.a:act B)`sch << filter_act`(snd exB) |] \
+\ Forall (%x. x:act (A||B)) sch ; \
+\ Filter (%a. a:act A)`sch << filter_act`(snd exA) ;\
+\ Filter (%a. a:act B)`sch << filter_act`(snd exB) |] \
 \ ==> stutter (asig_of B) (ProjB (mkex A B sch exA exB))";
 
 by (cut_facts_tac [stutterB_mkex] 1);
@@ -334,11 +334,11 @@
   --------------------------------------------------------------------------- *)
 
 goal thy "! exA exB s t. \
-\ Forall (%x.x:act (A||B)) sch & \
-\ Filter (%a.a:act A)`sch << filter_act`exA  &\
-\ Filter (%a.a:act B)`sch << filter_act`exB \
+\ Forall (%x. x:act (A||B)) sch & \
+\ Filter (%a. a:act A)`sch << filter_act`exA  &\
+\ Filter (%a. a:act B)`sch << filter_act`exB \
 \ --> Filter_ex2 (asig_of A)`(ProjA2`(snd (mkex A B sch (s,exA) (t,exB)))) =   \
-\     Zip`(Filter (%a.a:act A)`sch)`(Map snd`exA)";
+\     Zip`(Filter (%a. a:act A)`sch)`(Map snd`exA)";
 
 by (mkex_induct_tac "sch" "exA" "exB");
 
@@ -360,8 +360,8 @@
   --------------------------------------------------------------------------- *)
 
 goal thy "!! sch ex. \
-\ Filter (%a.a:act AB)`sch = filter_act`ex  \
-\ ==> ex = Zip`(Filter (%a.a:act AB)`sch)`(Map snd`ex)";
+\ Filter (%a. a:act AB)`sch = filter_act`ex  \
+\ ==> ex = Zip`(Filter (%a. a:act AB)`sch)`(Map snd`ex)";
 by (asm_full_simp_tac (!simpset addsimps [filter_act_def]) 1);
 by (rtac (Zip_Map_fst_snd RS sym) 1);
 qed"trick_against_eq_in_ass";
@@ -373,9 +373,9 @@
 
 
 goal thy "!!sch exA exB.\
-\ [| Forall (%a.a:act (A||B)) sch ; \
-\ Filter (%a.a:act A)`sch = filter_act`(snd exA)  ;\
-\ Filter (%a.a:act B)`sch = filter_act`(snd exB) |]\
+\ [| Forall (%a. a:act (A||B)) sch ; \
+\ Filter (%a. a:act A)`sch = filter_act`(snd exA)  ;\
+\ Filter (%a. a:act B)`sch = filter_act`(snd exB) |]\
 \ ==> Filter_ex (asig_of A) (ProjA (mkex A B sch exA exB)) = exA";
 by (asm_full_simp_tac (!simpset addsimps [ProjA_def,Filter_ex_def]) 1);
 by (pair_tac "exA" 1);
@@ -398,11 +398,11 @@
 
 
 goal thy "! exA exB s t. \
-\ Forall (%x.x:act (A||B)) sch & \
-\ Filter (%a.a:act A)`sch << filter_act`exA  &\
-\ Filter (%a.a:act B)`sch << filter_act`exB \
+\ Forall (%x. x:act (A||B)) sch & \
+\ Filter (%a. a:act A)`sch << filter_act`exA  &\
+\ Filter (%a. a:act B)`sch << filter_act`exB \
 \ --> Filter_ex2 (asig_of B)`(ProjB2`(snd (mkex A B sch (s,exA) (t,exB)))) =   \
-\     Zip`(Filter (%a.a:act B)`sch)`(Map snd`exB)";
+\     Zip`(Filter (%a. a:act B)`sch)`(Map snd`exB)";
 
 (* notice necessary change of arguments exA and exB *)
 by (mkex_induct_tac "sch" "exB" "exA");
@@ -417,9 +417,9 @@
 
 
 goal thy "!!sch exA exB.\
-\ [| Forall (%a.a:act (A||B)) sch ; \
-\ Filter (%a.a:act A)`sch = filter_act`(snd exA)  ;\
-\ Filter (%a.a:act B)`sch = filter_act`(snd exB) |]\
+\ [| Forall (%a. a:act (A||B)) sch ; \
+\ Filter (%a. a:act A)`sch = filter_act`(snd exA)  ;\
+\ Filter (%a. a:act B)`sch = filter_act`(snd exB) |]\
 \ ==> Filter_ex (asig_of B) (ProjB (mkex A B sch exA exB)) = exB";
 by (asm_full_simp_tac (!simpset addsimps [ProjB_def,Filter_ex_def]) 1);
 by (pair_tac "exA" 1);
@@ -439,9 +439,9 @@
 
 goal thy "!s t exA exB. \
 \ Forall (%x. x : act (A || B)) sch &\
-\ Filter (%a.a:act A)`sch << filter_act`exA  &\
-\ Filter (%a.a:act B)`sch << filter_act`exB \
-\  --> Forall (%x.fst x : act (A ||B))   \
+\ Filter (%a. a:act A)`sch << filter_act`exA  &\
+\ Filter (%a. a:act B)`sch << filter_act`exB \
+\  --> Forall (%x. fst x : act (A ||B))   \
 \        (snd (mkex A B sch (s,exA) (t,exB)))";
 
 by (mkex_induct_tac "sch" "exA" "exB");
@@ -456,8 +456,8 @@
 
 goal thy  
 "sch : schedules (A||B) = \
-\ (Filter (%a.a:act A)`sch : schedules A &\
-\  Filter (%a.a:act B)`sch : schedules B &\
+\ (Filter (%a. a:act A)`sch : schedules A &\
+\  Filter (%a. a:act B)`sch : schedules B &\
 \  Forall (%x. x:act (A||B)) sch)";
 
 by (simp_tac (!simpset addsimps [schedules_def, has_schedule_def]) 1);
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/IOA/meta_theory/CompoScheds.thy
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -67,8 +67,8 @@
        let schA = fst SchedsA; sigA = snd SchedsA; 
            schB = fst SchedsB; sigB = snd SchedsB       
        in
-       (    {sch. Filter (%a.a:actions sigA)`sch : schA}
-        Int {sch. Filter (%a.a:actions sigB)`sch : schB}
+       (    {sch. Filter (%a. a:actions sigA)`sch : schA}
+        Int {sch. Filter (%a. a:actions sigB)`sch : schB}
         Int {sch. Forall (%x. x:(actions sigA Un actions sigB)) sch},
         asig_comp sigA sigB)"
 
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/IOA/meta_theory/CompoTraces.ML
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -24,24 +24,24 @@
 \      | Def y => \
 \         (if y:act A then \
 \             (if y:act B then \ 
-\                   ((Takewhile (%a.a:int A)`schA) \
-\                         @@(Takewhile (%a.a:int B)`schB) \
+\                   ((Takewhile (%a. a:int A)`schA) \
+\                         @@(Takewhile (%a. a:int B)`schB) \
 \                              @@(y>>(mksch A B`xs   \
-\                                       `(TL`(Dropwhile (%a.a:int A)`schA))  \
-\                                       `(TL`(Dropwhile (%a.a:int B)`schB))  \
+\                                       `(TL`(Dropwhile (%a. a:int A)`schA))  \
+\                                       `(TL`(Dropwhile (%a. a:int B)`schB))  \
 \                    )))   \
 \              else  \
-\                 ((Takewhile (%a.a:int A)`schA)  \
+\                 ((Takewhile (%a. a:int A)`schA)  \
 \                      @@ (y>>(mksch A B`xs  \
-\                              `(TL`(Dropwhile (%a.a:int A)`schA))  \
+\                              `(TL`(Dropwhile (%a. a:int A)`schA))  \
 \                              `schB)))  \
 \              )   \
 \          else    \
 \             (if y:act B then  \ 
-\                 ((Takewhile (%a.a:int B)`schB)  \
+\                 ((Takewhile (%a. a:int B)`schB)  \
 \                       @@ (y>>(mksch A B`xs   \
 \                              `schA   \
-\                              `(TL`(Dropwhile (%a.a:int B)`schB))  \
+\                              `(TL`(Dropwhile (%a. a:int B)`schB))  \
 \                              )))  \
 \             else  \
 \               UU  \
@@ -62,8 +62,8 @@
 
 goal thy "!!x.[|x:act A;x~:act B|]  \
 \   ==> mksch A B`(x>>tr)`schA`schB = \
-\         (Takewhile (%a.a:int A)`schA) \
-\         @@ (x>>(mksch A B`tr`(TL`(Dropwhile (%a.a:int A)`schA)) \
+\         (Takewhile (%a. a:int A)`schA) \
+\         @@ (x>>(mksch A B`tr`(TL`(Dropwhile (%a. a:int A)`schA)) \
 \                             `schB))";
 by (rtac trans 1);
 by (stac mksch_unfold 1);
@@ -73,8 +73,8 @@
 
 goal thy "!!x.[|x~:act A;x:act B|] \
 \   ==> mksch A B`(x>>tr)`schA`schB = \
-\        (Takewhile (%a.a:int B)`schB)  \
-\         @@ (x>>(mksch A B`tr`schA`(TL`(Dropwhile (%a.a:int B)`schB))  \
+\        (Takewhile (%a. a:int B)`schB)  \
+\         @@ (x>>(mksch A B`tr`schA`(TL`(Dropwhile (%a. a:int B)`schB))  \
 \                            ))";
 by (rtac trans 1);
 by (stac mksch_unfold 1);
@@ -84,10 +84,10 @@
 
 goal thy "!!x.[|x:act A;x:act B|] \
 \   ==> mksch A B`(x>>tr)`schA`schB = \
-\            (Takewhile (%a.a:int A)`schA) \
-\         @@ ((Takewhile (%a.a:int B)`schB)  \
-\         @@ (x>>(mksch A B`tr`(TL`(Dropwhile (%a.a:int A)`schA)) \
-\                            `(TL`(Dropwhile (%a.a:int B)`schB))))  \
+\            (Takewhile (%a. a:int A)`schA) \
+\         @@ ((Takewhile (%a. a:int B)`schB)  \
+\         @@ (x>>(mksch A B`tr`(TL`(Dropwhile (%a. a:int A)`schA)) \
+\                            `(TL`(Dropwhile (%a. a:int B)`schB))))  \
 \             )";
 by (rtac trans 1);
 by (stac mksch_unfold 1);
@@ -208,7 +208,7 @@
 Delsimps [FiniteConc];
 
 goal thy "!! tr. [| Finite tr; is_asig(asig_of A); is_asig(asig_of B) |] ==> \
-\   ! x y. Forall (%x.x:act A) x & Forall (%x.x:act B) y & \
+\   ! x y. Forall (%x. x:act A) x & Forall (%x. x:act B) y & \
 \          Filter (%a. a:ext A)`x = Filter (%a. a:act A)`tr & \
 \          Filter (%a. a:ext B)`y = Filter (%a. a:act B)`tr &\
 \          Forall (%x. x:ext (A||B)) tr \
@@ -283,7 +283,7 @@
 Delsimps [FilterConc]; 
 
 goal thy " !!bs. [| Finite bs; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==>  \
-\! y.Forall (%x.x:act B) y & Forall (%x. x:act B & x~:act A) bs &\
+\! y. Forall (%x. x:act B) y & Forall (%x. x:act B & x~:act A) bs &\
 \    Filter (%a. a:ext B)`y = Filter (%a. a:act B)`(bs @@ z) \
 \    --> (? y1 y2.  (mksch A B`(bs @@ z)`x`y) = (y1 @@ (mksch A B`z`x`y2)) & \
 \                   Forall (%x. x:act B & x~:act A) y1 & \
@@ -312,7 +312,7 @@
 Addsimps [FilterConc]; 
 by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,not_ext_is_int_or_not_act]) 1);
 (* apply IH *)
-by (eres_inst_tac [("x","TL`(Dropwhile (%a.a:int B)`y)")] allE 1);
+by (eres_inst_tac [("x","TL`(Dropwhile (%a. a:int B)`y)")] allE 1);
 by (asm_full_simp_tac (!simpset addsimps [ForallTL,ForallDropwhile])1);
 by (REPEAT (etac exE 1));
 by (REPEAT (etac conjE 1));
@@ -321,7 +321,7 @@
 by (rotate_tac ~2 1); 
 by (Asm_full_simp_tac 1); 
 (* instantiate y1a and y2a *)
-by (res_inst_tac [("x","Takewhile (%a.a:int B)`y @@ a>>y1")] exI 1);
+by (res_inst_tac [("x","Takewhile (%a. a:int B)`y @@ a>>y1")] exI 1);
 by (res_inst_tac [("x","y2")] exI 1);
 (* elminate all obligations up to two depending on Conc_assoc *)
 by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ, intA_is_not_actB,
@@ -338,7 +338,7 @@
 
 
 goal thy " !!as. [| Finite as; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==>  \
-\! x.Forall (%x.x:act A) x & Forall (%x. x:act A & x~:act B) as &\
+\! x. Forall (%x. x:act A) x & Forall (%x. x:act A & x~:act B) as &\
 \    Filter (%a. a:ext A)`x = Filter (%a. a:act A)`(as @@ z) \
 \    --> (? x1 x2.  (mksch A B`(as @@ z)`x`y) = (x1 @@ (mksch A B`z`x2`y)) & \
 \                   Forall (%x. x:act A & x~:act B) x1 & \
@@ -367,7 +367,7 @@
 Addsimps [FilterConc]; 
 by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,not_ext_is_int_or_not_act]) 1);
 (* apply IH *)
-by (eres_inst_tac [("x","TL`(Dropwhile (%a.a:int A)`x)")] allE 1);
+by (eres_inst_tac [("x","TL`(Dropwhile (%a. a:int A)`x)")] allE 1);
 by (asm_full_simp_tac (!simpset addsimps [ForallTL,ForallDropwhile])1);
 by (REPEAT (etac exE 1));
 by (REPEAT (etac conjE 1));
@@ -376,7 +376,7 @@
 by (rotate_tac ~2 1); 
 by (Asm_full_simp_tac 1); 
 (* instantiate y1a and y2a *)
-by (res_inst_tac [("x","Takewhile (%a.a:int A)`x @@ a>>x1")] exI 1);
+by (res_inst_tac [("x","Takewhile (%a. a:int A)`x @@ a>>x1")] exI 1);
 by (res_inst_tac [("x","x2")] exI 1);
 (* elminate all obligations up to two depending on Conc_assoc *)
 by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ, intA_is_not_actB,
@@ -434,7 +434,7 @@
 by (rotate_tac ~2 2);
 by (rotate_tac ~2 3);
 by (asm_full_simp_tac (HOL_basic_ss addsimps [mksch_cons3]) 2);
-by (eres_inst_tac [("x","sb@@Takewhile (%a.a: int A)`a @@ Takewhile (%a.a:int B)`b@@(aaa>>nil)")] allE 2);
+by (eres_inst_tac [("x","sb@@Takewhile (%a. a: int A)`a @@ Takewhile (%a. a:int B)`b@@(aaa>>nil)")] allE 2);
 by (eres_inst_tac [("x","sa")] allE 2);
 by (asm_full_simp_tac (!simpset addsimps [Conc_assoc])2);
 
@@ -481,11 +481,11 @@
 goal thy 
 "!! A B. [| compatible A B; compatible B A;\
 \           is_asig(asig_of A); is_asig(asig_of B) |] ==> \
-\ ! schA schB. Forall (%x.x:act A) schA & Forall (%x.x:act B) schB & \
-\ Forall (%x.x:ext (A||B)) tr & \
-\ Filter (%a.a:act A)`tr << Filter (%a.a:ext A)`schA &\
-\ Filter (%a.a:act B)`tr << Filter (%a.a:ext B)`schB  \
-\ --> Filter (%a.a:ext (A||B))`(mksch A B`tr`schA`schB) = tr";
+\ ! schA schB. Forall (%x. x:act A) schA & Forall (%x. x:act B) schB & \
+\ Forall (%x. x:ext (A||B)) tr & \
+\ Filter (%a. a:act A)`tr << Filter (%a. a:ext A)`schA &\
+\ Filter (%a. a:act B)`tr << Filter (%a. a:ext B)`schB  \
+\ --> Filter (%a. a:ext (A||B))`(mksch A B`tr`schA`schB) = tr";
 
 by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1);
 
@@ -557,12 +557,12 @@
 
 goal thy "!! A B. [| compatible A B; compatible B A; \
 \ is_asig(asig_of A); is_asig(asig_of B) |] ==> \
-\ Forall (%x.x:ext (A||B)) tr & \
-\ Forall (%x.x:act A) schA & Forall (%x.x:act B) schB & \
-\ Filter (%a.a:ext A)`schA = Filter (%a.a:act A)`tr &\
-\ Filter (%a.a:ext B)`schB = Filter (%a.a:act B)`tr &\
+\ Forall (%x. x:ext (A||B)) tr & \
+\ Forall (%x. x:act A) schA & Forall (%x. x:act B) schB & \
+\ Filter (%a. a:ext A)`schA = Filter (%a. a:act A)`tr &\
+\ Filter (%a. a:ext B)`schB = Filter (%a. a:act B)`tr &\
 \ LastActExtsch A schA & LastActExtsch B schB  \
-\ --> Filter (%a.a:act A)`(mksch A B`tr`schA`schB) = schA";
+\ --> Filter (%a. a:act A)`(mksch A B`tr`schA`schB) = schA";
 
 by (res_inst_tac [("Q","%x. x:act B & x~:act A"),("x","tr")] take_lemma_less_induct 1);
 by (REPEAT (etac conjE 1));
@@ -613,7 +613,7 @@
 
 (* eliminate the B-only prefix *)
 
-by (subgoal_tac "(Filter (%a.a :act A)`y1) = nil" 1);
+by (subgoal_tac "(Filter (%a. a :act A)`y1) = nil" 1);
 by (etac ForallQFilterPnil 2);
 by (assume_tac 2);
 by (Fast_tac 2);
@@ -691,12 +691,12 @@
 
 goal thy "!! A B. [| compatible A B; compatible B A; \
 \ is_asig(asig_of A); is_asig(asig_of B) |] ==> \
-\ Forall (%x.x:ext (A||B)) tr & \
-\ Forall (%x.x:act A) schA & Forall (%x.x:act B) schB & \
-\ Filter (%a.a:ext A)`schA = Filter (%a.a:act A)`tr &\
-\ Filter (%a.a:ext B)`schB = Filter (%a.a:act B)`tr &\
+\ Forall (%x. x:ext (A||B)) tr & \
+\ Forall (%x. x:act A) schA & Forall (%x. x:act B) schB & \
+\ Filter (%a. a:ext A)`schA = Filter (%a. a:act A)`tr &\
+\ Filter (%a. a:ext B)`schB = Filter (%a. a:act B)`tr &\
 \ LastActExtsch A schA & LastActExtsch B schB  \
-\ --> Filter (%a.a:act A)`(mksch A B`tr`schA`schB) = schA";
+\ --> Filter (%a. a:act A)`(mksch A B`tr`schA`schB) = schA";
 
 by (strip_tac 1);
 by (rtac seq.take_lemma 1);
@@ -730,7 +730,7 @@
 (* second side: schA = nil *)
 by (eres_inst_tac [("A","A")] LastActExtimplnil 1);
 by (Asm_simp_tac 1);
-by (eres_inst_tac [("Q","%x.x:act B & x~:act A")] ForallQFilterPnil 1);
+by (eres_inst_tac [("Q","%x. x:act B & x~:act A")] ForallQFilterPnil 1);
 by (assume_tac 1);
 by (Fast_tac 1);
 
@@ -747,7 +747,7 @@
 (* schA = UU *)
 by (eres_inst_tac [("A","A")] LastActExtimplUU 1);
 by (Asm_simp_tac 1);
-by (eres_inst_tac [("Q","%x.x:act B & x~:act A")] ForallQFilterPUU 1);
+by (eres_inst_tac [("Q","%x. x:act B & x~:act A")] ForallQFilterPUU 1);
 by (assume_tac 1);
 by (Fast_tac 1);
 
@@ -771,7 +771,7 @@
 
 (* eliminate the B-only prefix *)
 
-by (subgoal_tac "(Filter (%a.a :act A)`y1) = nil" 1);
+by (subgoal_tac "(Filter (%a. a :act A)`y1) = nil" 1);
 by (etac ForallQFilterPnil 2);
 by (assume_tac 2);
 by (Fast_tac 2);
@@ -833,7 +833,7 @@
 
 (* assumption Forall schA *)
 by (dres_inst_tac [("s","schA"),
-                   ("P","Forall (%x.x:act A)")] subst 1);
+                   ("P","Forall (%x. x:act A)")] subst 1);
 by (assume_tac 1);
 by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ, int_is_act]) 1);
 
@@ -933,12 +933,12 @@
 
 goal thy "!! A B. [| compatible A B; compatible B A; \
 \ is_asig(asig_of A); is_asig(asig_of B) |] ==> \
-\ Forall (%x.x:ext (A||B)) tr & \
-\ Forall (%x.x:act A) schA & Forall (%x.x:act B) schB & \
-\ Filter (%a.a:ext A)`schA = Filter (%a.a:act A)`tr &\
-\ Filter (%a.a:ext B)`schB = Filter (%a.a:act B)`tr &\
+\ Forall (%x. x:ext (A||B)) tr & \
+\ Forall (%x. x:act A) schA & Forall (%x. x:act B) schB & \
+\ Filter (%a. a:ext A)`schA = Filter (%a. a:act A)`tr &\
+\ Filter (%a. a:ext B)`schB = Filter (%a. a:act B)`tr &\
 \ LastActExtsch A schA & LastActExtsch B schB  \
-\ --> Filter (%a.a:act B)`(mksch A B`tr`schA`schB) = schB";
+\ --> Filter (%a. a:act B)`(mksch A B`tr`schA`schB) = schB";
 
 by (strip_tac 1);
 by (rtac seq.take_lemma 1);
@@ -972,7 +972,7 @@
 (* second side: schA = nil *)
 by (eres_inst_tac [("A","B")] LastActExtimplnil 1);
 by (Asm_simp_tac 1);
-by (eres_inst_tac [("Q","%x.x:act A & x~:act B")] ForallQFilterPnil 1);
+by (eres_inst_tac [("Q","%x. x:act A & x~:act B")] ForallQFilterPnil 1);
 by (assume_tac 1);
 by (Fast_tac 1);
 
@@ -989,7 +989,7 @@
 (* schA = UU *)
 by (eres_inst_tac [("A","B")] LastActExtimplUU 1);
 by (Asm_simp_tac 1);
-by (eres_inst_tac [("Q","%x.x:act A & x~:act B")] ForallQFilterPUU 1);
+by (eres_inst_tac [("Q","%x. x:act A & x~:act B")] ForallQFilterPUU 1);
 by (assume_tac 1);
 by (Fast_tac 1);
 
@@ -1013,7 +1013,7 @@
 
 (* eliminate the A-only prefix *)
 
-by (subgoal_tac "(Filter (%a.a :act B)`x1) = nil" 1);
+by (subgoal_tac "(Filter (%a. a :act B)`x1) = nil" 1);
 by (etac ForallQFilterPnil 2);
 by (assume_tac 2);
 by (Fast_tac 2);
@@ -1075,7 +1075,7 @@
 
 (* assumption Forall schB *)
 by (dres_inst_tac [("s","schB"),
-                   ("P","Forall (%x.x:act B)")] subst 1);
+                   ("P","Forall (%x. x:act B)")] subst 1);
 by (assume_tac 1);
 by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ, int_is_act]) 1);
 
@@ -1173,8 +1173,8 @@
 "!! A B. [| is_trans_of A; is_trans_of B; compatible A B; compatible B A; \
 \           is_asig(asig_of A); is_asig(asig_of B)|] \
 \       ==>  tr: traces(A||B) = \
-\            (Filter (%a.a:act A)`tr : traces A &\
-\             Filter (%a.a:act B)`tr : traces B &\
+\            (Filter (%a. a:act A)`tr : traces A &\
+\             Filter (%a. a:act B)`tr : traces B &\
 \             Forall (%x. x:ext(A||B)) tr)";
 
 by (simp_tac (!simpset addsimps [traces_def,has_trace_def]) 1);
@@ -1182,12 +1182,12 @@
  
 (* ==> *) 
 (* There is a schedule of A *)
-by (res_inst_tac [("x","Filter (%a.a:act A)`sch")] bexI 1);
+by (res_inst_tac [("x","Filter (%a. a:act A)`sch")] bexI 1);
 by (asm_full_simp_tac (!simpset addsimps [compositionality_sch]) 2);
 by (asm_full_simp_tac (!simpset addsimps [compatibility_consequence1,
                   externals_of_par,ext1_ext2_is_not_act1]) 1);
 (* There is a schedule of B *)
-by (res_inst_tac [("x","Filter (%a.a:act B)`sch")] bexI 1);
+by (res_inst_tac [("x","Filter (%a. a:act B)`sch")] bexI 1);
 by (asm_full_simp_tac (!simpset addsimps [compositionality_sch]) 2);
 by (asm_full_simp_tac (!simpset addsimps [compatibility_consequence2,
                   externals_of_par,ext1_ext2_is_not_act2]) 1);
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/IOA/meta_theory/CompoTraces.thy
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -25,24 +25,24 @@
       | Def y => 
          (if y:act A then 
              (if y:act B then 
-                   ((Takewhile (%a.a:int A)`schA)
-                      @@ (Takewhile (%a.a:int B)`schB)
+                   ((Takewhile (%a. a:int A)`schA)
+                      @@ (Takewhile (%a. a:int B)`schB)
                            @@ (y>>(h`xs
-                                    `(TL`(Dropwhile (%a.a:int A)`schA))
-                                    `(TL`(Dropwhile (%a.a:int B)`schB))
+                                    `(TL`(Dropwhile (%a. a:int A)`schA))
+                                    `(TL`(Dropwhile (%a. a:int B)`schB))
                     )))
               else
-                 ((Takewhile (%a.a:int A)`schA)
+                 ((Takewhile (%a. a:int A)`schA)
                   @@ (y>>(h`xs
-                           `(TL`(Dropwhile (%a.a:int A)`schA))
+                           `(TL`(Dropwhile (%a. a:int A)`schA))
                            `schB)))
               )
           else 
              (if y:act B then 
-                 ((Takewhile (%a.a:int B)`schB)
+                 ((Takewhile (%a. a:int B)`schB)
                      @@ (y>>(h`xs
                               `schA
-                              `(TL`(Dropwhile (%a.a:int B)`schB))
+                              `(TL`(Dropwhile (%a. a:int B)`schB))
                               )))
              else
                UU
@@ -56,8 +56,8 @@
        let trA = fst TracesA; sigA = snd TracesA; 
            trB = fst TracesB; sigB = snd TracesB       
        in
-       (    {tr. Filter (%a.a:actions sigA)`tr : trA}
-        Int {tr. Filter (%a.a:actions sigB)`tr : trB}
+       (    {tr. Filter (%a. a:actions sigA)`tr : trA}
+        Int {tr. Filter (%a. a:actions sigB)`tr : trB}
         Int {tr. Forall (%x. x:(externals sigA Un externals sigB)) tr},
         asig_comp sigA sigB)"
 
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/IOA/meta_theory/Deadlock.ML
--- a/src/HOLCF/IOA/meta_theory/Deadlock.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Deadlock.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -10,8 +10,8 @@
                input actions may always be added to a schedule
 **********************************************************************************)
 
-goal thy "!! sch. [| Filter (%x.x:act A)`sch : schedules A; a:inp A; input_enabled A; Finite sch|] \
-\         ==> Filter (%x.x:act A)`sch @@ a>>nil : schedules A";
+goal thy "!! sch. [| Filter (%x. x:act A)`sch : schedules A; a:inp A; input_enabled A; Finite sch|] \
+\         ==> Filter (%x. x:act A)`sch @@ a>>nil : schedules A";
 by (asm_full_simp_tac (!simpset addsimps [schedules_def,has_schedule_def]) 1);
 by (safe_tac set_cs);
 by (forward_tac  [inp_is_act] 1);
@@ -52,7 +52,7 @@
 **********************************************************************************)
 
 goal thy "!! sch. [| a : local A; Finite sch; sch : schedules (A||B); \
-\            Filter (%x.x:act A)`(sch @@ a>>nil) : schedules A; compatible A B; input_enabled B |] \
+\            Filter (%x. x:act A)`(sch @@ a>>nil) : schedules A; compatible A B; input_enabled B |] \
 \          ==> (sch @@ a>>nil) : schedules (A||B)";
 
 by (asm_full_simp_tac (!simpset addsimps [compositionality_sch,locals_def]) 1);
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/IOA/meta_theory/Sequence.ML
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -543,7 +543,7 @@
 
 section "Last";
 
-goal thy "!! s.Finite s ==> s~=nil --> Last`s~=UU";
+goal thy "!! s. Finite s ==> s~=nil --> Last`s~=UU";
 by (Seq_Finite_induct_tac  1);
 by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
 qed"Finite_Last1";
@@ -790,11 +790,11 @@
 by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
 qed"Takewhile_idempotent";
 
-goal thy "Forall P s --> Takewhile (%x.Q x | (~P x))`s = Takewhile Q`s";
+goal thy "Forall P s --> Takewhile (%x. Q x | (~P x))`s = Takewhile Q`s";
 by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
 qed"ForallPTakewhileQnP";
 
-goal thy "Forall P s --> Dropwhile (%x.Q x | (~P x))`s = Dropwhile Q`s";
+goal thy "Forall P s --> Dropwhile (%x. Q x | (~P x))`s = Dropwhile Q`s";
 by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
 qed"ForallPDropwhileQnP";
 
@@ -807,7 +807,7 @@
 
 bind_thm("TakewhileConc",TakewhileConc1 RS mp);
 
-goal thy "!! s.Finite s ==> Forall P s --> Dropwhile P`(s @@ t) = Dropwhile P`t";
+goal thy "!! s. Finite s ==> Forall P s --> Dropwhile P`(s @@ t) = Dropwhile P`t";
 by (Seq_Finite_induct_tac 1);
 qed"DropwhileConc1";
 
@@ -905,7 +905,7 @@
 qed"take_reduction1";
 
 
-goal thy "!! n.[| x=y; s=t;!! k.k<n ==> seq_take k`y1 = seq_take k`y2|] \
+goal thy "!! n.[| x=y; s=t;!! k. k<n ==> seq_take k`y1 = seq_take k`y2|] \
 \ ==> seq_take n`(x @@ (s>>y1)) =  seq_take n`(y @@ (t>>y2))";
 
 by (auto_tac (!claset addSIs [take_reduction1 RS spec RS mp],!simpset));
@@ -927,7 +927,7 @@
 qed"take_reduction_less1";
 
 
-goal thy "!! n.[| x=y; s=t;!! k.k<n ==> seq_take k`y1 << seq_take k`y2|] \
+goal thy "!! n.[| x=y; s=t;!! k. k<n ==> seq_take k`y1 << seq_take k`y2|] \
 \ ==> seq_take n`(x @@ (s>>y1)) <<  seq_take n`(y @@ (t>>y2))";
 by (auto_tac (!claset addSIs [take_reduction_less1 RS spec RS mp],!simpset));
 qed"take_reduction_less";
@@ -1168,17 +1168,17 @@
 
 goal thy "!! s. Finite s ==>  \
 \         Forall (%x. (~P x) | (~ Q x)) s  \
-\         --> Filter (%x.P x & Q x)`s = nil";
+\         --> Filter (%x. P x & Q x)`s = nil";
 by (Seq_Finite_induct_tac 1);
 by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
 qed"Filter_lemma3";
 
 
 goal thy "Filter P`(Filter Q`s) = Filter (%x. P x & Q x)`s";
-by (res_inst_tac [("A1","%x.True") 
+by (res_inst_tac [("A1","%x. True") 
                  ,("Q1","%x.~(P x & Q x)"),("x1","s")]
                  (take_lemma_induct RS mp) 1);
-(* FIX: better support for A = %.True *)
+(* FIX: better support for A = %x. True *)
 by (Fast_tac 3);
 by (asm_full_simp_tac (!simpset addsimps [Filter_lemma1]) 1);
 by (asm_full_simp_tac (!simpset addsimps [Filter_lemma2,Filter_lemma3] 
@@ -1195,7 +1195,7 @@
 
 
 goal thy "Map f`(x@@y) = (Map f`x) @@ (Map f`y)";
-by (res_inst_tac [("A1","%x.True"),("x1","x")] (take_lemma_in_eq_out RS mp) 1);
+by (res_inst_tac [("A1","%x. True"),("x1","x")] (take_lemma_in_eq_out RS mp) 1);
 by (Auto_tac());
 qed"MapConc_takelemma";
 
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/IOA/meta_theory/Traces.ML
--- a/src/HOLCF/IOA/meta_theory/Traces.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Traces.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -67,7 +67,7 @@
 goal thy "is_exec_fragC A = (LAM ex. (%s. case ex of \
 \      nil => TT \
 \    | x##xs => (flift1 \ 
-\            (%p.Def ((s,p):trans_of A) andalso (is_exec_fragC A`xs) (snd p)) \
+\            (%p. Def ((s,p):trans_of A) andalso (is_exec_fragC A`xs) (snd p)) \
 \             `x) \
 \   ))";
 by (rtac trans 1);
@@ -163,7 +163,7 @@
 
 goal thy 
   "!! A. is_trans_of A ==> \
-\ ! s. is_exec_frag A (s,xs) --> Forall (%a.a:act A) (filter_act`xs)";
+\ ! s. is_exec_frag A (s,xs) --> Forall (%a. a:act A) (filter_act`xs)";
 
 by (pair_induct_tac "xs" [is_exec_frag_def,Forall_def,sforall_def] 1);
 (* main case *)
@@ -174,7 +174,7 @@
 
 goal thy 
   "!! A.[|  is_trans_of A; x:executions A |] ==> \
-\ Forall (%a.a:act A) (filter_act`(snd x))";
+\ Forall (%a. a:act A) (filter_act`(snd x))";
 
 by (asm_full_simp_tac (!simpset addsimps [executions_def]) 1);
 by (pair_tac "x" 1);
@@ -184,7 +184,7 @@
 
 goalw thy [schedules_def,has_schedule_def]
   "!! A.[|  is_trans_of A; x:schedules A |] ==> \
-\   Forall (%a.a:act A) x";
+\   Forall (%a. a:act A) x";
 
 by (fast_tac (!claset addSIs [exec_in_sig]) 1);
 qed"scheds_in_sig";
@@ -208,7 +208,7 @@
 
 (* second prefix notion for Finite x *)
 
-goal thy "! y s.is_exec_frag A (s,x@@y) --> is_exec_frag A (s,x)";
+goal thy "! y s. is_exec_frag A (s,x@@y) --> is_exec_frag A (s,x)";
 by (pair_induct_tac "x" [is_exec_frag_def] 1);
 by (strip_tac 1);
 by (Seq_case_simp_tac "s" 1);
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/IOA/meta_theory/Traces.thy
--- a/src/HOLCF/IOA/meta_theory/Traces.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Traces.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -67,7 +67,7 @@
   "is_exec_fragC A ==(fix`(LAM h ex. (%s. case ex of 
       nil => TT
     | x##xs => (flift1 
-            (%p.Def ((s,p):trans_of A) andalso (h`xs) (snd p)) 
+            (%p. Def ((s,p):trans_of A) andalso (h`xs) (snd p)) 
              `x)
    )))" 
 
@@ -96,7 +96,7 @@
 
 has_trace_def
   "has_trace ioa tr ==                                               
-     (? sch:schedules ioa. tr = Filter (%a.a:ext(ioa))`sch)"
+     (? sch:schedules ioa. tr = Filter (%a. a:ext(ioa))`sch)"
 
 traces_def
   "traces ioa == {tr. has_trace ioa tr}"
@@ -104,7 +104,7 @@
 
 mk_trace_def
   "mk_trace ioa == LAM tr. 
-     Filter (%a.a:ext(ioa))`(filter_act`tr)"
+     Filter (%a. a:ext(ioa))`(filter_act`tr)"
 
 
 (*  ------------------- Implementation ------------------------------ *)
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/Lift.ML
--- a/src/HOLCF/Lift.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Lift.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -22,7 +22,7 @@
 (* flift1 is continuous in a variable that occurs only 
    in the Def branch *)
 
-goal thy "!!f. [| !! a.cont (%y. (f y) a) |] ==> \
+goal thy "!!f. [| !! a. cont (%y. (f y) a) |] ==> \
 \          cont (%y. lift_case UU (f y))";
 by (rtac cont2cont_CF1L_rev 1);
 by (strip_tac 1);
@@ -34,7 +34,7 @@
 (* flift1 is continuous in a variable that occurs either 
    in the Def branch or in the argument *)
 
-goal thy "!!f. [| !! a.cont (%y. (f y) a); cont g|] ==> \
+goal thy "!!f. [| !! a. cont (%y. (f y) a); cont g|] ==> \
 \   cont (%y. lift_case UU (f y) (g y))";
 by (rtac cont2cont_app 1);
 back();
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/Lift2.ML
--- a/src/HOLCF/Lift2.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Lift2.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -9,7 +9,7 @@
 open Lift2;
 
 (* for compatibility with old HOLCF-Version *)
-qed_goal "inst_lift_po" thy "(op <<)=(%x y.x=y|x=Undef)"
+qed_goal "inst_lift_po" thy "(op <<)=(%x y. x=y|x=Undef)"
  (fn prems => 
         [
         (fold_goals_tac [less_lift_def]),
@@ -26,7 +26,7 @@
 
 bind_thm ("UU_lift_def",minimal_lift RS minimal2UU RS sym);
 
-qed_goal "least_lift" thy "? x::'a lift.!y.x<<y"
+qed_goal "least_lift" thy "? x::'a lift.!y. x<<y"
 (fn prems =>
         [
         (res_inst_tac [("x","Undef")] exI 1),
@@ -57,7 +57,7 @@
 
 goal Lift2.thy
 "!!Y. [|? j.~Y(j)=Undef;is_chain(Y::nat=>('a)lift)|] \
-\ ==> ? j.!i.j<i-->~Y(i)=Undef";
+\ ==> ? j.!i. j<i-->~Y(i)=Undef";
 by Safe_tac;
 by (Step_tac 1);
 by (strip_tac 1);
@@ -74,7 +74,7 @@
         "(! Y. is_chain(Y::nat=>('a)lift)-->(? n. max_in_chain n Y))";
 by (rewtac max_in_chain_def);  
 by (strip_tac 1);
-by (res_inst_tac [("P","!i.Y(i)=Undef")] case_split_thm  1);
+by (res_inst_tac [("P","!i. Y(i)=Undef")] case_split_thm  1);
 by (res_inst_tac [("x","0")] exI 1);
 by (strip_tac 1);
 by (rtac trans 1);
@@ -82,7 +82,7 @@
 by (rtac sym 1);
 by (etac spec 1); 
 
-by (subgoal_tac "!x y.x<<(y::('a)lift) --> x=Undef | x=y" 1);
+by (subgoal_tac "!x y. x<<(y::('a)lift) --> x=Undef | x=y" 1);
 by (simp_tac (!simpset addsimps [inst_lift_po]) 2);
 by (rtac (chain_mono2_po RS exE) 1); 
 by (Fast_tac 1); 
@@ -110,7 +110,7 @@
 (* Main Lemma: cpo_lift *)
 
 goal Lift2.thy  
-  "!!Y. is_chain(Y::nat=>('a)lift) ==> ? x.range(Y) <<|x";
+  "!!Y. is_chain(Y::nat=>('a)lift) ==> ? x. range(Y) <<|x";
 by (cut_inst_tac [] flat_imp_chain_finite_poo 1);
 by (Step_tac 1);
 by Safe_tac;
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/Lift3.ML
--- a/src/HOLCF/Lift3.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Lift3.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -80,7 +80,7 @@
                  section"UU and Def";             
 (* ---------------------------------------------------------- *)
 
-goal thy "x=UU | (? y.x=Def y)"; 
+goal thy "x=UU | (? y. x=Def y)"; 
 by (lift.induct_tac "x" 1);
 by (Asm_simp_tac 1);
 by (rtac disjI2 1);
@@ -100,7 +100,7 @@
 by (ALLGOALS Asm_simp_tac);
 qed "expand_lift_case";
 
-goal thy "(x~=UU)=(? y.x=Def y)";
+goal thy "(x~=UU)=(? y. x=Def y)";
 by (rtac iffI 1);
 by (rtac Lift_cases 1);
 by (REPEAT (fast_tac (HOL_cs addSIs lift.distinct) 1));
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/Pcpo.ML
--- a/src/HOLCF/Pcpo.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Pcpo.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -13,7 +13,7 @@
 (* derive the old rule minimal                                              *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goalw "UU_least" thy [ UU_def ] "!z.UU << z"
+qed_goalw "UU_least" thy [ UU_def ] "!z. UU << z"
 (fn prems => [ 
         (rtac (select_eq_Ex RS iffD2) 1),
         (rtac least 1)]);
@@ -83,7 +83,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "lub_equal" thy
-"[| is_chain(C1::(nat=>'a::cpo));is_chain(C2);!k.C1(k)=C2(k)|]\
+"[| is_chain(C1::(nat=>'a::cpo));is_chain(C2);!k. C1(k)=C2(k)|]\
 \       ==> lub(range(C1))=lub(range(C2))"
 (fn prems =>
         [
@@ -206,7 +206,7 @@
         ]);
 
 qed_goal "chain_UU_I" thy
-        "[|is_chain(Y);lub(range(Y))=UU|] ==> ! i.Y(i)=UU"
+        "[|is_chain(Y);lub(range(Y))=UU|] ==> ! i. Y(i)=UU"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -219,7 +219,7 @@
 
 
 qed_goal "chain_UU_I_inverse" thy 
-        "!i.Y(i::nat)=UU ==> lub(range(Y::(nat=>'a::pcpo)))=UU"
+        "!i. Y(i::nat)=UU ==> lub(range(Y::(nat=>'a::pcpo)))=UU"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -257,7 +257,7 @@
 
 qed_goal "chain_mono2" thy 
 "[|? j.~Y(j)=UU;is_chain(Y::nat=>'a::pcpo)|]\
-\ ==> ? j.!i.j<i-->~Y(i)=UU"
+\ ==> ? j.!i. j<i-->~Y(i)=UU"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -279,11 +279,11 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goalw "flat_imp_chain_finite" thy [max_in_chain_def]
-        "!Y::nat=>'a::flat.is_chain Y-->(? n.max_in_chain n Y)"
+        "!Y::nat=>'a::flat. is_chain Y-->(? n. max_in_chain n Y)"
  (fn _ =>
         [
         (strip_tac 1),
-        (case_tac "!i.Y(i)=UU" 1),
+        (case_tac "!i. Y(i)=UU" 1),
         (res_inst_tac [("x","0")] exI 1),
 	(Asm_simp_tac 1),
  	(Asm_full_simp_tac 1),
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/Pcpo.thy
--- a/src/HOLCF/Pcpo.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Pcpo.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -17,7 +17,7 @@
 (* ****************************** *)
 axclass pcpo < cpo
 
-  least         "? x.!y.x<<y"
+  least         "? x.!y. x<<y"
 
 consts
   UU            :: "'a::pcpo"        
@@ -26,16 +26,16 @@
   UU            :: "'a::pcpo"                           ("\\<bottom>")
 
 defs
-  UU_def        "UU == @x.!y.x<<y"       
+  UU_def        "UU == @x.!y. x<<y"       
 
 (* further useful classes for HOLCF domains *)
 
 axclass chfin<cpo
 
-chfin 	"!Y.is_chain Y-->(? n.max_in_chain n Y)"
+chfin 	"!Y. is_chain Y-->(? n. max_in_chain n Y)"
 
 axclass flat<pcpo
 
-ax_flat	 	"! x y.x << y --> (x = UU) | (x=y)"
+ax_flat	 	"! x y. x << y --> (x = UU) | (x=y)"
 
 end 
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/Porder.ML
--- a/src/HOLCF/Porder.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Porder.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -256,7 +256,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "lub_chain_maxelem" thy
-"[|? i.Y i=c;!i.Y i<<c|] ==> lub(range Y) = c"
+"[|? i. Y i=c;!i. Y i<<c|] ==> lub(range Y) = c"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -274,7 +274,7 @@
 (* the lub of a constant chain is the constant                              *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goal "lub_const" thy "range(%x.c) <<| c"
+qed_goal "lub_const" thy "range(%x. c) <<| c"
  (fn prems =>
         [
         (rtac is_lubI 1),
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/Porder.thy
--- a/src/HOLCF/Porder.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Porder.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -24,7 +24,7 @@
 
 translations
 
-  "LUB x. t"	== "lub(range(%x.t))"
+  "LUB x. t"	== "lub(range(%x. t))"
 
 syntax (symbols)
 
@@ -33,14 +33,14 @@
 defs
 
 (* class definitions *)
-is_ub           "S  <| x == ! y.y:S --> y<<x"
+is_ub           "S  <| x == ! y. y:S --> y<<x"
 is_lub          "S <<| x == S <| x & (! u. S <| u  --> x << u)"
 
 (* Arbitrary chains are total orders    *)                  
 is_tord         "is_tord S == ! x y. x:S & y:S --> (x<<y | y<<x)"
 
 (* Here we use countable chains and I prefer to code them as functions! *)
-is_chain        "is_chain F == (! i.F(i) << F(Suc(i)))"
+is_chain        "is_chain F == (! i. F(i) << F(Suc(i)))"
 
 (* finite chains, needed for monotony of continouous functions *)
 max_in_chain_def "max_in_chain i C == ! j. i <= j --> C(i) = C(j)" 
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/Porder0.ML
--- a/src/HOLCF/Porder0.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Porder0.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -12,7 +12,7 @@
 (* ------------------------------------------------------------------------ *)
 (* minimal fixes least element                                              *)
 (* ------------------------------------------------------------------------ *)
-bind_thm("minimal2UU",allI RS (prove_goal thy "!x::'a::po.uu<<x==>uu=(@u.!y.u<<y)"
+bind_thm("minimal2UU",allI RS (prove_goal thy "!x::'a::po. uu<<x==>uu=(@u.!y. u<<y)"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/Sprod2.ML
--- a/src/HOLCF/Sprod2.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Sprod2.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -9,7 +9,7 @@
 open Sprod2;
 
 (* for compatibility with old HOLCF-Version *)
-qed_goal "inst_sprod_po" thy "(op <<)=(%x y.Isfst x<<Isfst y&Issnd x<<Issnd y)"
+qed_goal "inst_sprod_po" thy "(op <<)=(%x y. Isfst x<<Isfst y&Issnd x<<Issnd y)"
  (fn prems => 
         [
 	(fold_goals_tac [less_sprod_def]),
@@ -28,7 +28,7 @@
 
 bind_thm ("UU_sprod_def",minimal_sprod RS minimal2UU RS sym);
 
-qed_goal "least_sprod" thy "? x::'a**'b.!y.x<<y"
+qed_goal "least_sprod" thy "? x::'a**'b.!y. x<<y"
 (fn prems =>
         [
         (res_inst_tac [("x","Ispair UU UU")] exI 1),
@@ -96,7 +96,7 @@
 
 qed_goal "lub_sprod" Sprod2.thy 
 "[|is_chain(S)|] ==> range(S) <<| \
-\ Ispair (lub(range(%i.Isfst(S i)))) (lub(range(%i.Issnd(S i))))"
+\ Ispair (lub(range(%i. Isfst(S i)))) (lub(range(%i. Issnd(S i))))"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -123,7 +123,7 @@
 
 
 qed_goal "cpo_sprod" Sprod2.thy 
-        "is_chain(S::nat=>'a**'b)==>? x.range(S)<<| x"
+        "is_chain(S::nat=>'a**'b)==>? x. range(S)<<| x"
 (fn prems =>
         [
         (cut_facts_tac prems 1),
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/Sprod3.ML
--- a/src/HOLCF/Sprod3.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Sprod3.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -134,7 +134,7 @@
         (res_inst_tac [("f1","Ispair")] (arg_cong RS cong) 1),
         (rtac sym 1),
         (rtac lub_chain_maxelem 1),
-        (res_inst_tac [("P","%j.Y(j)~=UU")] exE 1),
+        (res_inst_tac [("P","%j. Y(j)~=UU")] exE 1),
         (rtac (not_all RS iffD1) 1),
         (res_inst_tac [("Q","lub(range(Y)) = UU")] contrapos 1),
         (atac 1),
@@ -315,7 +315,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goalw "beta_cfun_sprod" thy [spair_def]
-        "(LAM x y.Ispair x y)`a`b = Ispair a b"
+        "(LAM x y. Ispair x y)`a`b = Ispair a b"
  (fn prems =>
         [
         (stac beta_cfun 1),
@@ -564,7 +564,7 @@
 
 qed_goalw "lub_sprod2" thy [sfst_def,ssnd_def,spair_def]
 "[|is_chain(S)|] ==> range(S) <<| \
-\ (| lub(range(%i.sfst`(S i))), lub(range(%i.ssnd`(S i))) |)"
+\ (| lub(range(%i. sfst`(S i))), lub(range(%i. ssnd`(S i))) |)"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/Sprod3.thy
--- a/src/HOLCF/Sprod3.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Sprod3.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -24,10 +24,10 @@
         "(|x, y|)"      == "spair`x`y"
 
 defs
-spair_def       "spair  == (LAM x y.Ispair x y)"
-sfst_def        "sfst   == (LAM p.Isfst p)"
-ssnd_def        "ssnd   == (LAM p.Issnd p)"     
-ssplit_def      "ssplit == (LAM f. strictify`(LAM p.f`(sfst`p)`(ssnd`p)))"
+spair_def       "spair  == (LAM x y. Ispair x y)"
+sfst_def        "sfst   == (LAM p. Isfst p)"
+ssnd_def        "ssnd   == (LAM p. Issnd p)"     
+ssplit_def      "ssplit == (LAM f. strictify`(LAM p. f`(sfst`p)`(ssnd`p)))"
 
 end
 
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/Ssum0.thy
--- a/src/HOLCF/Ssum0.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Ssum0.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -15,7 +15,7 @@
  "Sinr_Rep == (%b.%x y p.(b~=UU --> y=b & ~p))"
 
 typedef (Ssum)  ('a, 'b) "++" (infixr 10) = 
-	"{f.(? a.f=Sinl_Rep(a))|(? b.f=Sinr_Rep(b))}"
+	"{f.(? a. f=Sinl_Rep(a))|(? b. f=Sinr_Rep(b))}"
 
 syntax (symbols)
   "++"		:: [type, type] => type	("(_ \\<oplus>/ _)" [21, 20] 20)
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/Ssum1.thy
--- a/src/HOLCF/Ssum1.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Ssum1.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -12,10 +12,10 @@
 
 defs
   less_ssum_def "(op <<) == (%s1 s2.@z.
-         (! u x.s1=Isinl u & s2=Isinl x --> z = u << x)
-        &(! v y.s1=Isinr v & s2=Isinr y --> z = v << y)
-        &(! u y.s1=Isinl u & s2=Isinr y --> z = (u = UU))
-        &(! v x.s1=Isinr v & s2=Isinl x --> z = (v = UU)))"
+         (! u x. s1=Isinl u & s2=Isinl x --> z = u << x)
+        &(! v y. s1=Isinr v & s2=Isinr y --> z = v << y)
+        &(! u y. s1=Isinl u & s2=Isinr y --> z = (u = UU))
+        &(! v x. s1=Isinr v & s2=Isinl x --> z = (v = UU)))"
 
 end
 
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/Ssum2.ML
--- a/src/HOLCF/Ssum2.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Ssum2.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -10,10 +10,10 @@
 
 (* for compatibility with old HOLCF-Version *)
 qed_goal "inst_ssum_po" thy "(op <<)=(%s1 s2.@z.\
-\         (! u x.s1=Isinl u & s2=Isinl x --> z = u << x)\
-\        &(! v y.s1=Isinr v & s2=Isinr y --> z = v << y)\
-\        &(! u y.s1=Isinl u & s2=Isinr y --> z = (u = UU))\
-\        &(! v x.s1=Isinr v & s2=Isinl x --> z = (v = UU)))"
+\         (! u x. s1=Isinl u & s2=Isinl x --> z = u << x)\
+\        &(! v y. s1=Isinr v & s2=Isinr y --> z = v << y)\
+\        &(! u y. s1=Isinl u & s2=Isinr y --> z = (u = UU))\
+\        &(! v x. s1=Isinr v & s2=Isinl x --> z = (v = UU)))"
  (fn prems => 
         [
         (fold_goals_tac [less_ssum_def]),
@@ -67,7 +67,7 @@
 
 bind_thm ("UU_ssum_def",minimal_ssum RS minimal2UU RS sym);
 
-qed_goal "least_ssum" thy "? x::'a++'b.!y.x<<y"
+qed_goal "least_ssum" thy "? x::'a++'b.!y. x<<y"
 (fn prems =>
         [
         (res_inst_tac [("x","Isinl UU")] exI 1),
@@ -174,7 +174,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "ssum_lemma1" thy 
-"[|~(!i.? x.Y(i::nat)=Isinl(x))|] ==> (? i.! x.Y(i)~=Isinl(x))"
+"[|~(!i.? x. Y(i::nat)=Isinl(x))|] ==> (? i.! x. Y(i)~=Isinl(x))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -199,7 +199,7 @@
 
 qed_goal "ssum_lemma3" thy 
 "[|is_chain(Y);(? i x. Y(i)=Isinr(x::'b) & (x::'b)~=UU)|] ==>\
-\ (!i.? y.Y(i)=Isinr(y))"
+\ (!i.? y. Y(i)=Isinr(y))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -231,7 +231,7 @@
         ]);
 
 qed_goal "ssum_lemma4" thy 
-"is_chain(Y) ==> (!i.? x.Y(i)=Isinl(x))|(!i.? y.Y(i)=Isinr(y))"
+"is_chain(Y) ==> (!i.? x. Y(i)=Isinl(x))|(!i.? y. Y(i)=Isinr(y))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -249,7 +249,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "ssum_lemma5" thy 
-"z=Isinl(x)==> Isinl((Iwhen (LAM x.x) (LAM y.UU))(z)) = z"
+"z=Isinl(x)==> Isinl((Iwhen (LAM x. x) (LAM y. UU))(z)) = z"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -264,7 +264,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "ssum_lemma6" thy 
-"z=Isinr(x)==> Isinr((Iwhen (LAM y.UU) (LAM x.x))(z)) = z"
+"z=Isinr(x)==> Isinr((Iwhen (LAM y. UU) (LAM x. x))(z)) = z"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -279,7 +279,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "ssum_lemma7" thy 
-"[|Isinl(x) << z; x~=UU|] ==> ? y.z=Isinl(y) & y~=UU"
+"[|Isinl(x) << z; x~=UU|] ==> ? y. z=Isinl(y) & y~=UU"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -297,7 +297,7 @@
         ]);
 
 qed_goal "ssum_lemma8" thy 
-"[|Isinr(x) << z; x~=UU|] ==> ? y.z=Isinr(y) & y~=UU"
+"[|Isinr(x) << z; x~=UU|] ==> ? y. z=Isinr(y) & y~=UU"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -317,9 +317,9 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "lub_ssum1a" thy 
-"[|is_chain(Y);(!i.? x.Y(i)=Isinl(x))|] ==>\
+"[|is_chain(Y);(!i.? x. Y(i)=Isinl(x))|] ==>\
 \ range(Y) <<|\
-\ Isinl(lub(range(%i.(Iwhen (LAM x.x) (LAM y.UU))(Y i))))"
+\ Isinl(lub(range(%i.(Iwhen (LAM x. x) (LAM y. UU))(Y i))))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -358,9 +358,9 @@
 
 
 qed_goal "lub_ssum1b" thy 
-"[|is_chain(Y);(!i.? x.Y(i)=Isinr(x))|] ==>\
+"[|is_chain(Y);(!i.? x. Y(i)=Isinr(x))|] ==>\
 \ range(Y) <<|\
-\ Isinr(lub(range(%i.(Iwhen (LAM y.UU) (LAM x.x))(Y i))))"
+\ Isinr(lub(range(%i.(Iwhen (LAM y. UU) (LAM x. x))(Y i))))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -413,7 +413,7 @@
 *)
 
 qed_goal "cpo_ssum" thy 
-        "is_chain(Y::nat=>'a ++'b) ==> ? x.range(Y) <<|x"
+        "is_chain(Y::nat=>'a ++'b) ==> ? x. range(Y) <<|x"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/Ssum3.ML
--- a/src/HOLCF/Ssum3.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Ssum3.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -156,7 +156,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "ssum_lemma9" Ssum3.thy 
-"[| is_chain(Y); lub(range(Y)) = Isinl(x)|] ==> !i.? x.Y(i)=Isinl(x)"
+"[| is_chain(Y); lub(range(Y)) = Isinl(x)|] ==> !i.? x. Y(i)=Isinl(x)"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -174,7 +174,7 @@
 
 
 qed_goal "ssum_lemma10" Ssum3.thy 
-"[| is_chain(Y); lub(range(Y)) = Isinr(x)|] ==> !i.? x.Y(i)=Isinr(x)"
+"[| is_chain(Y); lub(range(Y)) = Isinr(x)|] ==> !i.? x. Y(i)=Isinr(x)"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -615,7 +615,7 @@
 
 qed_goalw "thelub_ssum2b" Ssum3.thy [sinl_def,sinr_def,sswhen_def] 
 "[| is_chain(Y); !i.? x. Y(i) = sinr`x |] ==>\ 
-\   lub(range(Y)) = sinr`(lub(range(%i. sswhen`(LAM y. UU)`(LAM x.x)`(Y i))))"
+\   lub(range(Y)) = sinr`(lub(range(%i. sswhen`(LAM y. UU)`(LAM x. x)`(Y i))))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -641,7 +641,7 @@
         ]);
 
 qed_goalw "thelub_ssum2a_rev" Ssum3.thy [sinl_def,sinr_def] 
-        "[| is_chain(Y); lub(range(Y)) = sinl`x|] ==> !i.? x.Y(i)=sinl`x"
+        "[| is_chain(Y); lub(range(Y)) = sinl`x|] ==> !i.? x. Y(i)=sinl`x"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -655,7 +655,7 @@
         ]);
 
 qed_goalw "thelub_ssum2b_rev" Ssum3.thy [sinl_def,sinr_def] 
-        "[| is_chain(Y); lub(range(Y)) = sinr`x|] ==> !i.? x.Y(i)=sinr`x"
+        "[| is_chain(Y); lub(range(Y)) = sinr`x|] ==> !i.? x. Y(i)=sinr`x"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -670,8 +670,8 @@
 
 qed_goal "thelub_ssum3" Ssum3.thy  
 "is_chain(Y) ==>\ 
-\   lub(range(Y)) = sinl`(lub(range(%i. sswhen`(LAM x. x)`(LAM y.UU)`(Y i))))\
-\ | lub(range(Y)) = sinr`(lub(range(%i. sswhen`(LAM y. UU)`(LAM x.x)`(Y i))))"
+\   lub(range(Y)) = sinl`(lub(range(%i. sswhen`(LAM x. x)`(LAM y. UU)`(Y i))))\
+\ | lub(range(Y)) = sinr`(lub(range(%i. sswhen`(LAM y. UU)`(LAM x. x)`(Y i))))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/Ssum3.thy
--- a/src/HOLCF/Ssum3.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Ssum3.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -17,11 +17,11 @@
 
 defs
 
-sinl_def        "sinl   == (LAM x.Isinl(x))"
-sinr_def        "sinr   == (LAM x.Isinr(x))"
-sswhen_def      "sswhen   == (LAM f g s.Iwhen(f)(g)(s))"
+sinl_def        "sinl   == (LAM x. Isinl(x))"
+sinr_def        "sinr   == (LAM x. Isinr(x))"
+sswhen_def      "sswhen   == (LAM f g s. Iwhen(f)(g)(s))"
 
 translations
-"case s of sinl`x => t1 | sinr`y => t2" == "sswhen`(LAM x.t1)`(LAM y.t2)`s"
+"case s of sinl`x => t1 | sinr`y => t2" == "sswhen`(LAM x. t1)`(LAM y. t2)`s"
 
 end
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/Tr.thy
--- a/src/HOLCF/Tr.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Tr.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -34,9 +34,9 @@
   TT_def      "TT==Def True"
   FF_def      "FF==Def False"
   neg_def     "neg == flift2 Not"
-  ifte_def    "Icifte == (LAM b t e.flift1(%b.if b then t else e)`b)"
-  andalso_def "trand == (LAM x y.If x then y else FF fi)"
-  orelse_def  "tror == (LAM x y.If x then TT else y fi)"
+  ifte_def    "Icifte == (LAM b t e. flift1(%b. if b then t else e)`b)"
+  andalso_def "trand == (LAM x y. If x then y else FF fi)"
+  orelse_def  "tror == (LAM x y. If x then TT else y fi)"
   If2_def     "If2 Q x y == If Q then x else y fi"
 
 end
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/Up1.thy
--- a/src/HOLCF/Up1.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Up1.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -23,7 +23,7 @@
 defs
   Iup_def     "Iup x == Abs_Up(Inr(x))"
   Ifup_def    "Ifup(f)(x)== case Rep_Up(x) of Inl(y) => UU | Inr(z) => f`z"
-  less_up_def "(op <<) == (%x1 x2.case Rep_Up(x1) of                 
+  less_up_def "(op <<) == (%x1 x2. case Rep_Up(x1) of                 
                Inl(y1) => True          
              | Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False       
                                             | Inr(z2) => y2<<z2))"
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/Up2.ML
--- a/src/HOLCF/Up2.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Up2.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -9,7 +9,7 @@
 open Up2;
 
 (* for compatibility with old HOLCF-Version *)
-qed_goal "inst_up_po" thy "(op <<)=(%x1 x2.case Rep_Up(x1) of \               
+qed_goal "inst_up_po" thy "(op <<)=(%x1 x2. case Rep_Up(x1) of \               
 \               Inl(y1) => True \
 \             | Inr(y2) => (case Rep_Up(x2) of Inl(z1) => False \
 \                                            | Inr(z2) => y2<<z2))"
@@ -31,7 +31,7 @@
 
 bind_thm ("UU_up_def",minimal_up RS minimal2UU RS sym);
 
-qed_goal "least_up" thy "? x::'a u.!y.x<<y"
+qed_goal "least_up" thy "? x::'a u.!y. x<<y"
 (fn prems =>
         [
         (res_inst_tac [("x","Abs_Up(Inl ())")] exI 1),
@@ -99,7 +99,7 @@
 (* Some kind of surjectivity lemma                                          *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goal "up_lemma1" thy  "z=Iup(x) ==> Iup(Ifup(LAM x.x)(z)) = z"
+qed_goal "up_lemma1" thy  "z=Iup(x) ==> Iup(Ifup(LAM x. x)(z)) = z"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -111,8 +111,8 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "lub_up1a" thy 
-"[|is_chain(Y);? i x.Y(i)=Iup(x)|] ==>\
-\ range(Y) <<| Iup(lub(range(%i.(Ifup (LAM x.x) (Y(i))))))"
+"[|is_chain(Y);? i x. Y(i)=Iup(x)|] ==>\
+\ range(Y) <<| Iup(lub(range(%i.(Ifup (LAM x. x) (Y(i))))))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -183,7 +183,7 @@
 *)
 
 qed_goal "cpo_up" thy 
-        "is_chain(Y::nat=>('a)u) ==> ? x.range(Y) <<|x"
+        "is_chain(Y::nat=>('a)u) ==> ? x. range(Y) <<|x"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/Up3.ML
--- a/src/HOLCF/Up3.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Up3.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -274,7 +274,7 @@
         ]);
 
 
-qed_goal "up_lemma2" thy  " (? x.z = up`x) = (z~=UU)"
+qed_goal "up_lemma2" thy  " (? x. z = up`x) = (z~=UU)"
  (fn prems =>
         [
         (rtac iffI 1),
@@ -317,7 +317,7 @@
 
 qed_goal "thelub_up3" thy  
 "is_chain(Y) ==> lub(range(Y)) = UU |\
-\                lub(range(Y)) = up`(lub(range(%i. fup`(LAM x.x)`(Y i))))"
+\                lub(range(Y)) = up`(lub(range(%i. fup`(LAM x. x)`(Y i))))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/Up3.thy
--- a/src/HOLCF/Up3.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Up3.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -14,12 +14,12 @@
 
 constdefs  
         up  :: "'a -> ('a)u"
-       "up  == (LAM x.Iup(x))"
+       "up  == (LAM x. Iup(x))"
         fup :: "('a->'c)-> ('a)u -> 'c"
-       "fup == (LAM f p.Ifup(f)(p))"
+       "fup == (LAM f p. Ifup(f)(p))"
 
 translations
-"case l of up`x => t1" == "fup`(LAM x.t1)`l"
+"case l of up`x => t1" == "fup`(LAM x. t1)`l"
 
 end
 
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/ex/Dlist.ML
--- a/src/HOLCF/ex/Dlist.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/ex/Dlist.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -5,7 +5,7 @@
 (* ------------------------------------------------------------------------- *)
 
 bind_thm ("lmap_def2", fix_prover2 Dlist.thy lmap_def 
-        "lmap = (LAM f s.case s of dnil => dnil | x ## l => f`x ## lmap`f`l )");
+        "lmap = (LAM f s. case s of dnil => dnil | x ## l => f`x ## lmap`f`l )");
 
 (* ------------------------------------------------------------------------- *)
 (* recursive  properties   of lmap                                           *)
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/ex/Dnat.ML
--- a/src/HOLCF/ex/Dnat.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/ex/Dnat.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -47,7 +47,7 @@
 val iterator_rews = 
 	[iterator1, iterator2, iterator3];
 
-val dnat_flat = prove_goal Dnat.thy "!x y::dnat.x<<y --> x=UU | x=y" 
+val dnat_flat = prove_goal Dnat.thy "!x y::dnat. x<<y --> x=UU | x=y" 
 (fn _ => [
 	(rtac allI 1),
 	(res_inst_tac [("x","x")] dnat.ind 1),
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/ex/Focus_ex.ML
--- a/src/HOLCF/ex/Focus_ex.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/ex/Focus_ex.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -63,7 +63,7 @@
 by (REPEAT (etac conjE 1));
 by (etac conjI 1);
 by (strip_tac 1);
-by (res_inst_tac [("x","fix`(LAM k.csnd`(f`<x,k>))")] exI 1);
+by (res_inst_tac [("x","fix`(LAM k. csnd`(f`<x,k>))")] exI 1);
 by (rtac conjI 1);
  by (asm_simp_tac HOLCF_ss 1);
  by (rtac trans 1);
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/ex/Focus_ex.thy
--- a/src/HOLCF/ex/Focus_ex.thy	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/ex/Focus_ex.thy	Fri Oct 10 19:02:28 1997 +0200
@@ -131,6 +131,6 @@
 
 def_g		"def_g g == (? f.
 			is_f f  & 
-	      		g = (LAM x. cfst`(f`<x,fix`(LAM  k.csnd`(f`<x,k>))>)))" 
+	      		g = (LAM x. cfst`(f`<x,fix`(LAM  k. csnd`(f`<x,k>))>)))" 
 
 end
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/ex/Hoare.ML
--- a/src/HOLCF/ex/Hoare.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/ex/Hoare.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -20,7 +20,7 @@
         ]);
 
 val hoare_lemma3 = prove_goal HOLCF.thy 
-" (!k.b1`(iterate k g x) = TT) | (? k. b1`(iterate k g x)~=TT)"
+" (!k. b1`(iterate k g x) = TT) | (? k. b1`(iterate k g x)~=TT)"
  (fn prems =>
         [
         (fast_tac HOL_cs 1)
@@ -177,8 +177,8 @@
 *)
 
 val hoare_lemma11 = prove_goal Hoare.thy 
-"(? n.b1`(iterate n g x) ~= TT) ==>\
-\ k=Least(%n.b1`(iterate n g x) ~= TT) & b1`(iterate k g x)=FF \
+"(? n. b1`(iterate n g x) ~= TT) ==>\
+\ k=Least(%n. b1`(iterate n g x) ~= TT) & b1`(iterate k g x)=FF \
 \ --> p`x = iterate k g x"
  (fn prems =>
         [
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/ex/Loop.ML
--- a/src/HOLCF/ex/Loop.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/ex/Loop.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -40,7 +40,7 @@
         ]);
 
 val while_unfold2 = prove_goal Loop.thy 
-        "!x.while`b`g`x = while`b`g`(iterate k (step`b`g) x)"
+        "!x. while`b`g`x = while`b`g`(iterate k (step`b`g) x)"
  (fn prems =>
         [
         (nat_ind_tac "k" 1),
@@ -83,7 +83,7 @@
 (* --------------------------------------------------------------------------- *)
 
 val loop_lemma1 = prove_goal Loop.thy
-"[|? y.b`y=FF; iterate k (step`b`g) x = UU|]==>iterate(Suc k) (step`b`g) x=UU"
+"[|? y. b`y=FF; iterate k (step`b`g) x = UU|]==>iterate(Suc k) (step`b`g) x=UU"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -98,7 +98,7 @@
         ]);
 
 val loop_lemma2 = prove_goal Loop.thy
-"[|? y.b`y=FF;iterate (Suc k) (step`b`g) x ~=UU |]==>\
+"[|? y. b`y=FF;iterate (Suc k) (step`b`g) x ~=UU |]==>\
 \iterate k (step`b`g) x ~=UU"
  (fn prems =>
         [
@@ -111,7 +111,7 @@
 
 val loop_lemma3 = prove_goal Loop.thy
 "[|!x. INV x & b`x=TT & g`x~=UU --> INV (g`x);\
-\? y.b`y=FF; INV x|] ==>\
+\? y. b`y=FF; INV x|] ==>\
 \iterate k (step`b`g) x ~=UU --> INV (iterate k (step`b`g) x)"
  (fn prems =>
         [
@@ -266,7 +266,7 @@
 
 val loop_inv = prove_goal Loop.thy
 "[| P(x);\
-\   !!y.P y ==> INV y;\
+\   !!y. P y ==> INV y;\
 \   !!y.[| INV y; b`y=TT; g`y~=UU|] ==> INV (g`y);\
 \   !!y.[| INV y; b`y=FF|]==> Q y;\
 \   while`b`g`x ~= UU |] ==> Q (while`b`g`x)"
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/ex/Stream.ML
--- a/src/HOLCF/ex/Stream.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/ex/Stream.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -140,7 +140,7 @@
 	(rtac refl 1)
 	]);
 
-qed_goal "chain_stream_take" thy "is_chain (%i.stream_take i`s)" (fn _ => [
+qed_goal "chain_stream_take" thy "is_chain (%i. stream_take i`s)" (fn _ => [
 	rtac is_chainI 1,
 	subgoal_tac "!i s. stream_take i`s << stream_take (Suc i)`s" 1,
 	fast_tac HOL_cs 1,
@@ -189,7 +189,7 @@
 *)
 
 val stream_take_lemma3 = prove_goal thy 
- "!x xs.x~=UU --> stream_take n`(x && xs) = x && xs --> stream_take n`xs=xs"
+ "!x xs. x~=UU --> stream_take n`(x && xs) = x && xs --> stream_take n`xs=xs"
  (fn prems => [
 	(nat_ind_tac "n" 1),
 	(asm_simp_tac (HOL_ss addsimps stream.take_rews) 1),
diff -r 22bbc1676768 -r b55686a7b22c src/HOLCF/ex/loeckx.ML
--- a/src/HOLCF/ex/loeckx.ML	Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/ex/loeckx.ML	Fri Oct 10 19:02:28 1997 +0200
@@ -3,7 +3,7 @@
 (* Loeckx & Sieber S.88                                 *)
 
 val prems = goalw Fix.thy [Ifix_def]
-"Ifix F= lub (range (%i.%G.iterate i G UU)) F";
+"Ifix F= lub (range (%i.%G. iterate i G UU)) F";
 by (stac thelub_fun 1);
 by (rtac ch2ch_fun 1);
 back();
@@ -48,15 +48,15 @@
 
 val prems = goal Fix.thy  "cont(Ifix)";
 by (res_inst_tac 
- [("t","Ifix"),("s","(%f.lub(range(%j.(LAM f. iterate j f UU)`f)))")]
+ [("t","Ifix"),("s","(%f. lub(range(%j.(LAM f. iterate j f UU)`f)))")]
   ssubst 1);
 by (rtac ext 1);
 by (rewtac Ifix_def );
 by (subgoal_tac 
-  "range(% i.iterate i f UU) = range(%j.(LAM f. iterate j f UU)`f)" 1);
+  "range(% i. iterate i f UU) = range(%j.(LAM f. iterate j f UU)`f)" 1);
 by (etac arg_cong 1);
 by (subgoal_tac 
-        "(% i.iterate i f UU) = (%j.(LAM f. iterate j f UU)`f)" 1);
+        "(% i. iterate i f UU) = (%j.(LAM f. iterate j f UU)`f)" 1);
 by (etac arg_cong 1);
 by (rtac ext 1);
 by (stac beta_cfun 1);
@@ -79,7 +79,7 @@
 (* the proof in little steps *)
 
 val prems = goal Fix.thy  
-"(% i.iterate i f UU) = (%j.(LAM f. iterate j f UU)`f)";
+"(% i. iterate i f UU) = (%j.(LAM f. iterate j f UU)`f)";
 by (rtac ext 1);
 by (stac beta_cfun 1);
 by (rtac  cont2cont_CF1L 1);
@@ -88,7 +88,7 @@
 val fix_lemma1 = result();
 
 val prems = goal Fix.thy  
-" Ifix = (%f.lub(range(%j.(LAM f.iterate j f UU)`f)))";
+" Ifix = (%f. lub(range(%j.(LAM f. iterate j f UU)`f)))";
 by (rtac ext 1);
 by (rewtac Ifix_def ); 
 by (stac fix_lemma1 1);