ex/Term.ML

 
 (*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)}) \
-\               |] ==> R(x.zs)  \
+\               |] ==> R(x$zs)  \
 \    |] ==> R(M)";
 by (rtac (major RS (Term_def RS def_induct)) 1);
 by (rtac Term_fun_mono 1);
 by (REPEAT (eresolve_tac ([uprodE, ssubst, minor] @
  		([Int_lower1,Int_lower2] RL [List_mono RS subsetD])) 1));
 val Term_induct = result();
 
 (*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);
 by (REPEAT (ares_tac prems 1));
 val Term_induct2 = result();

 val term_induct = result();
 
 (*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);
 by (rtac list_induct 1);  (*types force good instantiation*)
 by (ALLGOALS (asm_simp_tac (list_all_ss addsimps prems)));

 
 (* c : A <*> List(Term(A)) ==> c : Term(A) *)
 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();
 
 
 (*** Term_rec -- by wf recursion on pred_Sexp ***)

 by (asm_simp_tac (list_all_ss addsimps [trancl_pred_SexpD1, cut_apply]) 1);
 val Abs_map_lemma = result();
 
 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
       [prem2 RS Abs_map_lemma RS spec RS mp, pred_SexpI2 RS r_into_trancl,
        prem1, prem2 RS rev_subsetD, List_subset_Sexp,