changeset 33317 | b4534348b8fd |
parent 33035 | 15eab423e573 |
child 33339 | d41f77196338 |
--- a/src/HOL/Tools/TFL/rules.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/HOL/Tools/TFL/rules.ML Thu Oct 29 17:58:26 2009 +0100 @@ -807,7 +807,7 @@ (prover names) (ss0 addsimps [cut_lemma'] addeqcongs congs) ctm val th2 = equal_elim th1 th in - (th2, List.filter (not o restricted) (!tc_list)) + (th2, filter_out restricted (!tc_list)) end;