diff -r 61f39dcc1685 -r b93cc55cb7ab Subst/Subst.ML
--- a/Subst/Subst.ML	Fri Dec 02 10:26:59 1994 +0100
+++ b/Subst/Subst.ML	Fri Dec 02 11:43:20 1994 +0100
@@ -18,9 +18,9 @@
 in val subst_rews = map mk_thm 
 ["Const(c) <| al = Const(c)",
  "Comb(t,u) <| al = Comb(t <| al, u <| al)",
- "Nil <> bl = bl",
+ "[] <> bl = bl",
  "<a,b>#al <> bl = <a,b <| bl> # (al <> bl)",
- "sdom(Nil) = {}",
+ "sdom([]) = {}",
  "sdom(<a,b>#al) = if(Var(a)=b,sdom(al) Int Compl({a}),sdom(al) Un {a})"
 ];
    (* This rewrite isn't always desired *)
@@ -31,7 +31,7 @@
 
 (**** Substitutions ****)
 
-goal Subst.thy "t <| Nil = t";
+goal Subst.thy "t <| [] = t";
 by (uterm_ind_tac "t" 1);
 by (ALLGOALS (asm_simp_tac (subst_ss addsimps [Var_subst])));
 qed "subst_Nil";
@@ -95,7 +95,7 @@
 
 (**** Composition of Substitutions ****)
 
-goal Subst.thy "s <> Nil = s";
+goal Subst.thy "s <> [] = s";
 by (alist_ind_tac "s" 1);
 by (ALLGOALS (asm_simp_tac (subst_ss addsimps [subst_Nil])));
 qed "comp_Nil";