src/HOL/Tools/TFL/rules.ML

     val names = OldTerm.add_term_names (term_of ctm, [])
     val th1 = MetaSimplifier.rewrite_cterm(false,true,false)
       (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;
 
 
 fun prove strict (ptm, tac) =
   let