Subst/unifier.ML

--- a/Subst/unifier.ML	Thu Feb 24 14:45:57 1994 +0100
+++ b/Subst/unifier.ML	Wed Mar 02 12:26:55 1994 +0100
@@ -25,7 +25,7 @@
 
 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;
 
@@ -49,7 +49,7 @@
 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);
@@ -85,7 +85,7 @@
 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);
@@ -114,8 +114,8 @@
 
 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);
@@ -141,8 +141,8 @@
 
 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);
@@ -167,10 +167,10 @@
 (*                                                                           *)
 (*  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);   *)
@@ -191,7 +191,7 @@
 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();