| changeset 20348 | d59364649bcc |
| parent 20168 | ed7bced29e1b |
| child 20547 | 796ae7fa1049 |
--- a/src/HOL/Algebra/ringsimp.ML Mon Aug 07 17:43:51 2006 +0200 +++ b/src/HOL/Algebra/ringsimp.ML Tue Aug 08 08:18:59 2006 +0200 @@ -18,7 +18,7 @@ (** Theory and context data **) fun struct_eq ((s1, ts1), (s2, ts2)) = - (s1 = s2) andalso equal_lists (op aconv) (ts1, ts2); + (s1 = s2) andalso eq_list (op aconv) (ts1, ts2); structure AlgebraData = GenericDataFun (struct