Subst/alist.ML

--- a/Subst/alist.ML	Thu Feb 24 14:45:57 1994 +0100
+++ b/Subst/alist.ML	Wed Mar 02 12:26:55 1994 +0100
@@ -19,15 +19,15 @@
                             (fn _ => [simp_tac alist_ss 1])
   in map mk_thm 
      ["alist_rec(Nil,c,d) = c",
-      "alist_rec(Cons(<a,b>,al),c,d) = d(a,b,al,alist_rec(al,c,d))",
+      "alist_rec(<a,b>#al,c,d) = d(a,b,al,alist_rec(al,c,d))",
       "assoc(v,d,Nil) = d",
-      "assoc(v,d,Cons(<a,b>,al)) = if(v=a,b,assoc(v,d,al))"] end;
+      "assoc(v,d,<a,b>#al) = if(v=a,b,assoc(v,d,al))"] end;
 
 (*********)
 
 val prems = goal AList.thy
     "[| P(Nil);   \
-\       !!x y xs. P(xs) ==> P(Cons(<x,y>,xs)) |]  ==> P(l)";
+\       !!x y xs. P(xs) ==> P(<x,y>#xs) |]  ==> P(l)";
 by (list_ind_tac "l" 1);
 by (resolve_tac prems 1);
 by (rtac PairE 1);
@@ -43,7 +43,7 @@
 
 (*
 val prems = goal AList.thy
-    "[| P(Nil);  !! x y xs. P(xs) --> P(Cons(<x,y>,xs)) |] ==> P(a)";
+    "[| 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));
 val alist_induct2 = result();