small updates because datatype list is now used. In particular Nil -> []

--- a/Subst/AList.ML	Fri Dec 02 10:26:59 1994 +0100
+++ b/Subst/AList.ML	Fri Dec 02 11:43:20 1994 +0100
@@ -7,28 +7,19 @@
 
 open AList;
 
-(*********)
-
-val al_defs = [alist_rec_def,assoc_def];
-
-val alist_ss = prod_ss addsimps [Nil_not_Cons,Cons_not_Nil,Cons_Cons_eq,
-                                list_rec_Nil,list_rec_Cons];
-
 val al_rews = 
-  let fun mk_thm s = prove_goalw AList.thy al_defs s 
-                            (fn _ => [simp_tac alist_ss 1])
+  let fun mk_thm s = prove_goalw AList.thy [alist_rec_def,assoc_def] s 
+                            (fn _ => [simp_tac list_ss 1])
   in map mk_thm 
-     ["alist_rec(Nil,c,d) = c",
+     ["alist_rec([],c,d) = c",
       "alist_rec(<a,b>#al,c,d) = d(a,b,al,alist_rec(al,c,d))",
-      "assoc(v,d,Nil) = d",
+      "assoc(v,d,[]) = d",
       "assoc(v,d,<a,b>#al) = if(v=a,b,assoc(v,d,al))"] end;
 
-(*********)
-
 val prems = goal AList.thy
-    "[| P(Nil);   \
+    "[| P([]);   \
 \       !!x y xs. P(xs) ==> P(<x,y>#xs) |]  ==> P(l)";
-by (list_ind_tac "l" 1);
+by (list.induct_tac "l" 1);
 by (resolve_tac prems 1);
 by (rtac PairE 1);
 by (etac ssubst 1);
@@ -40,13 +31,3 @@
 fun alist_ind_tac a M = 
     EVERY [res_inst_tac [("l",a)] alist_induct M,
 	   rename_last_tac a ["1"] (M+1)];
-
-(*
-val prems = goal AList.thy
-    "[| P(Nil);  !! x y xs. P(xs) --> P(<x,y>#xs) |] ==> P(a)";
-by (alist_ind_tac "a" 1);
-by (ALLGOALS (cut_facts_tac prems THEN' fast_tac HOL_cs));
-qed "alist_induct2";
-
-add_inds alist_induct2;
-*)

--- a/Subst/AList.thy	Fri Dec 02 10:26:59 1994 +0100
+++ b/Subst/AList.thy	Fri Dec 02 11:43:20 1994 +0100
@@ -14,7 +14,7 @@
 
 rules
 
-  alist_rec_def "alist_rec(al,b,c) == list_rec(al, b, split(c))"
+  alist_rec_def "alist_rec(al,b,c) == list_rec(b, split(c), al)"
 
   assoc_def     "assoc(v,d,al) == alist_rec(al,d,%x y xs g.if(v=x,y,g))"
 

--- 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";

--- 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";