diff -r 4cc9149dc675 -r d27056ec0a5a Subst/AList.ML --- a/Subst/AList.ML Thu Aug 18 11:30:27 1994 +0200 +++ b/Subst/AList.ML Thu Aug 18 11:40:54 1994 +0200 @@ -1,8 +1,8 @@ -(* Title: Substitutions/alist.ML +(* Title: Substitutions/AList.ML Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge -For alist.thy. +For AList.thy. *) open AList; @@ -11,7 +11,7 @@ val al_defs = [alist_rec_def,assoc_def]; -val alist_ss = pair_ss addsimps [Nil_not_Cons,Cons_not_Nil,Cons_Cons_eq, +val alist_ss = prod_ss addsimps [Nil_not_Cons,Cons_not_Nil,Cons_Cons_eq, list_rec_Nil,list_rec_Cons]; val al_rews =