Subst/unifier.ML

 by (simp_tac (subst_ss addsimps [Unifier_iff]) 1);
 val Unifier_Comb = result() RS mp RS conjE;
 
 goal Unifier.thy
   "~v : vars_of(t) --> ~v : vars_of(u) -->Unifier(s,t,u) --> \
-\  Unifier(Cons(<v,r>,s),t,u)";
+\  Unifier(<v,r>#s,t,u)";
 by (simp_tac (subst_ss addsimps [Unifier_iff,repl_invariance]) 1);
 val Cons_Unifier = result() RS mp RS mp RS mp;
 
 (**** Most General Unifiers ****)
 

 by (asm_simp_tac (subst_ss addsimps [subst_comp]) 1);
 by (fast_tac (set_cs addIs [comp_Nil RS sym RS subst_refl]) 1);
 val MGU_iff = result();
 
 val [prem] = goal Unifier.thy
-     "~ Var(v) <: t ==> MGUnifier(Cons(<v,t>,Nil),Var(v),t)";
+     "~ Var(v) <: t ==> MGUnifier(<v,t>#Nil,Var(v),t)";
 by (simp_tac (subst_ss addsimps [MGU_iff,MoreGen_iff,Unifier_iff]) 1);
 by (REPEAT_SOME (step_tac set_cs));
 by (etac subst 1);
 by (etac ssubst_subst2 2);
 by (rtac (Cons_trivial RS subst_sym) 1);

 
 goal Unifier.thy "Idem(Nil)";
 by (simp_tac (subst_ss addsimps [raw_Idem_iff,refl RS subst_refl]) 1);
 val Idem_Nil = result();
 
-goal Unifier.thy "~ (Var(v) <: t) --> Idem(Cons(<v,t>,Nil))";
+goal Unifier.thy "~ (Var(v) <: t) --> Idem(<v,t>#Nil)";
 by (simp_tac (subst_ss addsimps [Var_subst,vars_iff_occseq,Idem_iff,srange_iff]
                        setloop (split_tac [expand_if])) 1);
 by (fast_tac set_cs 1);
 val Var_Idem = result() RS mp;
 

 by (fast_tac (set_cs addEs [subst_subst2]) 1);
 val lemma_lemma = result();
 
 val prems = goal Unifier.thy 
     "x : sdom(s) -->  ~x : srange(s) --> \
-\   ~vars_of(Var(x) <| s<>Cons(<x,Var(x)>,s)) = \
-\      vars_of(Var(x) <| Cons(<x,Var(x)>,s))";
+\   ~vars_of(Var(x) <| s<> <x,Var(x)>#s) = \
+\      vars_of(Var(x) <| <x,Var(x)>#s)";
 by (simp_tac (subst_ss addsimps [not_equal_iff]) 1);
 by (REPEAT (resolve_tac [impI,disjI2] 1));
 by(res_inst_tac [("x","x")] exI 1);
 br conjI 1;
 by (asm_simp_tac (subst_ss addsimps [Var_elim,subst_comp,repl_invariance]) 1);

 by (simp_tac (set_ss addsimps prems) 1);
 val not_cong = result();
 
 val prems = goal Unifier.thy 
    "~w=x --> x : vars_of(Var(w) <| s) --> w : sdom(s) --> ~w : srange(s) --> \
-\   ~vars_of(Var(w) <| s<>Cons(<x,Var(w)>,s)) = \
-\   vars_of(Var(w) <| Cons(<x,Var(w)>,s))";
+\   ~vars_of(Var(w) <| s<> <x,Var(w)>#s) = \
+\   vars_of(Var(w) <| <x,Var(w)>#s)";
 by (simp_tac (subst_ss addsimps [not_equal_iff]) 1);
 by (REPEAT (resolve_tac [impI,disjI1] 1));
 by(res_inst_tac [("x","w")] exI 1);
 by (ALLGOALS (asm_simp_tac (subst_ss addsimps  [Var_elim,subst_comp,
                 vars_var_iff RS not_cong RS iffD2 RS repl_invariance]) ));

 
 (*************** Correctness of a simple unification algorithm ***************)
 (*                                                                           *)
 (*  fun unify Const(m) Const(n) = if m=n then Nil else Fail                  *)
 (*    | unify Const(m) _        = Fail                                       *)
-(*    | unify Var(v)   t        = if Var(v)<:t then Fail else Cons(<v,t>,Nil)*)
+(*    | unify Var(v)   t        = if Var(v)<:t then Fail else <v,t>#Nil      *)
 (*    | unify Comb(t,u) Const(n) = Fail                                      *)
 (*    | unify Comb(t,u) Var(v)  = if Var(v) <: Comb(t,u) then Fail           *)
-(*                                               else Cons(<v,Comb(t,u>,Nil) *)
+(*                                               else <v,Comb(t,u>#Nil       *)
 (*    | unify Comb(t,u) Comb(v,w) = let s = unify t v                        *)
 (*                                  in if s=Fail then Fail                   *)
 (*                                               else unify (u<|s) (w<|s);   *)
 
 (**** Cases for the partial correctness of the algorithm ****)

 goal Unifier.thy "~m=n --> (ALL l.~Unifier(l,Const(m),Const(n)))";
 by (simp_tac (subst_ss addsimps[Unifier_iff]) 1);
 val Unify2 = result() RS mp;
 
 val [prem] = goalw Unifier.thy [MGIUnifier_def] 
- "~Var(v) <: t ==> MGIUnifier(Cons(<v,t>,Nil),Var(v),t)";
+ "~Var(v) <: t ==> MGIUnifier(<v,t>#Nil,Var(v),t)";
 by (fast_tac (HOL_cs addSIs [prem RS MGUnifier_Var,prem RS Var_Idem]) 1);
 val Unify3 = result();
 
 val [prem] = goal Unifier.thy "Var(v) <: t ==> (ALL l.~Unifier(l,Var(v),t))";
 by (simp_tac (subst_ss addsimps