changeset 15570 | 8d8c70b41bab |
parent 0 | a5a9c433f639 |
child 15574 | b1d1b5bfc464 |
--- a/src/Provers/typedsimp.ML Thu Mar 03 09:22:35 2005 +0100 +++ b/src/Provers/typedsimp.ML Thu Mar 03 12:43:01 2005 +0100 @@ -70,7 +70,7 @@ handle THM _ => (simp_rls, rl :: other_rls); (*Given the list rls, return the pair (simp_rls, other_rls).*) -fun process_rules rls = foldr add_rule (rls, ([],[])); +fun process_rules rls = Library.foldr add_rule (rls, ([],[])); (*Given list of rewrite rules, return list of both forms, reject others*) fun process_rewrites rls =