diff -r 61f39dcc1685 -r b93cc55cb7ab Subst/Unifier.ML
--- a/Subst/Unifier.ML	Fri Dec 02 10:26:59 1994 +0100
+++ b/Subst/Unifier.ML	Fri Dec 02 11:43:20 1994 +0100
@@ -35,7 +35,7 @@
 by (rtac refl 1);
 qed "MoreGen_iff";
 
-goal Unifier.thy  "Nil >> s";
+goal Unifier.thy  "[] >> s";
 by (simp_tac (subst_ss addsimps [MoreGen_iff]) 1);
 by (fast_tac (set_cs addIs [refl RS subst_refl]) 1);
 qed "MoreGen_Nil";
@@ -49,7 +49,7 @@
 qed "MGU_iff";
 
 val [prem] = goal Unifier.thy
-     "~ Var(v) <: t ==> MGUnifier(<v,t>#Nil,Var(v),t)";
+     "~ Var(v) <: t ==> MGUnifier([<v,t>],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);
@@ -81,11 +81,11 @@
                                 invariance,dom_range_disjoint])1);
 qed "Idem_iff";
 
-goal Unifier.thy "Idem(Nil)";
+goal Unifier.thy "Idem([])";
 by (simp_tac (subst_ss addsimps [raw_Idem_iff,refl RS subst_refl]) 1);
 qed "Idem_Nil";
 
-goal Unifier.thy "~ (Var(v) <: t) --> Idem(<v,t>#Nil)";
+goal Unifier.thy "~ (Var(v) <: t) --> Idem([<v,t>])";
 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);
@@ -181,7 +181,7 @@
 by (safe_tac (HOL_cs addSEs ([sym]@([spec] RL [mp]))));
 qed "Unify_comm";
 
-goal Unifier.thy "MGIUnifier(Nil,Const(n),Const(n))";
+goal Unifier.thy "MGIUnifier([],Const(n),Const(n))";
 by (simp_tac (subst_ss addsimps
 	      [MGIU_iff,MGU_iff,Unifier_iff,subst_eq_iff,Idem_Nil]) 1);
 qed "Unify1";
@@ -191,7 +191,7 @@
 val Unify2 = store_thm("Unify2", result() RS mp);
 
 val [prem] = goalw Unifier.thy [MGIUnifier_def] 
- "~Var(v) <: t ==> MGIUnifier(<v,t>#Nil,Var(v),t)";
+ "~Var(v) <: t ==> MGIUnifier([<v,t>],Var(v),t)";
 by (fast_tac (HOL_cs addSIs [prem RS MGUnifier_Var,prem RS Var_Idem]) 1);
 qed "Unify3";