Subst/AList.ML

 val al_rews = 
   let fun mk_thm s = prove_goalw AList.thy al_defs s 
                             (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);
 by (etac ssubst 1);
 by (resolve_tac prems 1);

     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(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();
 
 add_inds alist_induct2;