changeset 33317 | b4534348b8fd |
parent 33245 | 65232054ffd0 |
child 33339 | d41f77196338 |
--- a/src/HOL/Tools/TFL/post.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/HOL/Tools/TFL/post.ML Thu Oct 29 17:58:26 2009 +0100 @@ -71,7 +71,7 @@ | _ => r RS P_imp_P_eq_True (*Is this the best way to invoke the simplifier??*) -fun rewrite L = rewrite_rule (map mk_meta_eq (List.filter(not o id_thm) L)) +fun rewrite L = rewrite_rule (map mk_meta_eq (filter_out id_thm L)) fun join_assums th = let val thy = Thm.theory_of_thm th