--- a/src/HOL/Integ/Equiv.ML Wed Sep 11 18:45:33 1996 +0200 +++ b/src/HOL/Integ/Equiv.ML Wed Sep 11 18:46:07 1996 +0200 @@ -8,6 +8,8 @@ Equivalence relations in HOL Set Theory *) +val RSLIST = curry (op MRS); + open Equiv; Delrules [equalityI];