diff -r 69d815b0e1eb -r 21291189b51e ex/Term.ML
--- a/ex/Term.ML	Thu Feb 24 14:45:57 1994 +0100
+++ b/ex/Term.ML	Wed Mar 02 12:26:55 1994 +0100
@@ -40,7 +40,7 @@
 val [major,minor] = goal Term.thy 
     "[| M: Term(A);  \
 \       !!x zs. [| x: A;  zs: List(Term(A));  zs: List({x.R(x)}) \
-\               |] ==> R(x.zs)  \
+\               |] ==> R(x$zs)  \
 \    |] ==> R(M)";
 by (rtac (major RS (Term_def RS def_induct)) 1);
 by (rtac Term_fun_mono 1);
@@ -51,9 +51,9 @@
 (*Induction on Term(A) followed by induction on List *)
 val major::prems = goal Term.thy
     "[| M: Term(A);  \
-\       !!x.      [| x: A |] ==> R(x.NIL);  \
-\       !!x z zs. [| x: A;  z: Term(A);  zs: List(Term(A));  R(x.zs)  \
-\                 |] ==> R(x . CONS(z,zs))  \
+\       !!x.      [| x: A |] ==> R(x$NIL);  \
+\       !!x z zs. [| x: A;  z: Term(A);  zs: List(Term(A));  R(x$zs)  \
+\                 |] ==> R(x $ CONS(z,zs))  \
 \    |] ==> R(M)";
 by (rtac (major RS Term_induct) 1);
 by (etac List_induct 1);
@@ -97,7 +97,7 @@
 (*Induction for the abstract type 'a term*)
 val prems = goal Term.thy 
     "[| !!x. R(App(x,Nil));  \
-\       !!x t ts. R(App(x,ts)) ==> R(App(x, Cons(t,ts)))  \
+\       !!x t ts. R(App(x,ts)) ==> R(App(x, t#ts))  \
 \    |] ==> R(t)";
 by (rtac term_induct 1);  (*types force good instantiation*)
 by (etac rev_mp 1);
@@ -117,7 +117,7 @@
 val TermI = standard (Term_unfold RS equalityD2 RS subsetD);
 
 (*The constant APP is not declared; it is simply . *)
-val prems = goal Term.thy "[| M: A;  N : List(Term(A)) |] ==> M.N : Term(A)";
+val prems = goal Term.thy "[| M: A;  N : List(Term(A)) |] ==> M$N : Term(A)";
 by (REPEAT (resolve_tac (prems@[TermI, ListI, uprodI]) 1));
 val APP_I = result();
 
@@ -143,7 +143,7 @@
 
 val [prem1,prem2,A_subset_Sexp] = goal Term.thy
     "[| M: Sexp;  N: List(Term(A));  A<=Sexp |] ==> \
-\    Term_rec(M.N, d) = d(M, N, Abs_map(%Z. Term_rec(Z,d), N))";
+\    Term_rec(M$N, d) = d(M, N, Abs_map(%Z. Term_rec(Z,d), N))";
 by (rtac (Term_rec_unfold RS trans) 1);
 by (rtac (Split RS trans) 1);
 by (simp_tac (HOL_ss addsimps