Subst/Subst.ML

                                  (fn _ => [simp_tac raw_subst_ss 1])
 in val subst_rews = map mk_thm 
 ["Const(c) <| al = Const(c)",
  "Comb(t,u) <| al = Comb(t <| al, u <| al)",
  "Nil <> bl = bl",
- "Cons(<a,b>,al) <> bl = Cons(<a,b <| bl>, al <> bl)",
+ "<a,b>#al <> bl = <a,b <| bl> # (al <> bl)",
  "sdom(Nil) = {}",
- "sdom(Cons(<a,b>,al)) = if(Var(a)=b,sdom(al) Int Compl({a}),sdom(al) Un {a})"
+ "sdom(<a,b>#al) = if(Var(a)=b,sdom(al) Int Compl({a}),sdom(al) Un {a})"
 ];
    (* This rewrite isn't always desired *)
    val Var_subst = mk_thm "Var(x) <| al = assoc(x,Var(x),al)";
 end;
 

 goal Subst.thy "t <: u --> t <| s <: u <| s";
 by (uterm_ind_tac "u" 1);
 by (ALLGOALS (asm_simp_tac subst_ss));
 val subst_mono = result() RS mp;
 
-goal Subst.thy  "~ (Var(v) <: t) --> t <| Cons(<v,t <| s>,s) = t <| s";
+goal Subst.thy  "~ (Var(v) <: t) --> t <| <v,t <| s>#s = t <| s";
 by (imp_excluded_middle_tac "t = Var(v)" 1);
 by (res_inst_tac [("P",
-    "%x.~x=Var(v) --> ~(Var(v) <: x) --> x <| Cons(<v,t<|s>,s)=x<|s")]
+    "%x.~x=Var(v) --> ~(Var(v) <: x) --> x <| <v,t<|s>#s=x<|s")]
     uterm_induct 2);
 by (ALLGOALS (simp_tac (subst_ss addsimps [Var_subst])));
 by (fast_tac HOL_cs 1);
 val Var_not_occs = result() RS mp;
 

 by (REPEAT (etac rev_mp 3));
 by (ALLGOALS (asm_simp_tac subst_ss));
 by (ALLGOALS (fast_tac HOL_cs));
 val agreement = result();
 
-goal Subst.thy   "~ v: vars_of(t) --> t <| Cons(<v,u>,s) = t <| s";
+goal Subst.thy   "~ v: vars_of(t) --> t <| <v,u>#s = t <| s";
 by(simp_tac(subst_ss addsimps [agreement,Var_subst]
                      setloop (split_tac [expand_if])) 1);
 val repl_invariance = result() RS mp;
 
 val asms = goal Subst.thy 
-     "v : vars_of(t) --> w : vars_of(t <| Cons(<v,Var(w)>,s))";
+     "v : vars_of(t) --> w : vars_of(t <| <v,Var(w)>#s)";
 by (uterm_ind_tac "t" 1);
 by (ALLGOALS (asm_simp_tac (subst_ss addsimps [Var_subst])));
 val Var_in_subst = result() RS mp;
 
 (**** Equality between Substitutions ****)

 
 goal Subst.thy "q <> r <> s =s= q <> (r <> s)";
 by (simp_tac (subst_ss addsimps [subst_eq_iff,subst_comp]) 1);
 val comp_assoc = result();
 
-goal Subst.thy "Cons(<w,Var(w) <| s>,s) =s= s"; 
+goal Subst.thy "<w,Var(w) <| s>#s =s= s"; 
 by (rtac (allI RS (subst_eq_iff RS iffD2)) 1);
 by (uterm_ind_tac "t" 1);
 by (REPEAT (etac rev_mp 3));
 by (ALLGOALS (simp_tac (subst_ss addsimps[Var_subst]
                                  setloop (split_tac [expand_if]))));