else

        else

          let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in

          let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in

            all_facts ctxt ho_atp reserved add chained_ths css_table

            all_facts ctxt ho_atp reserved add chained_ths css_table

            |> filter_out (member Thm.eq_thm_prop del o snd)

            |> filter_out (member Thm.eq_thm_prop del o snd)

            |> maybe_filter_no_atps ctxt

            |> maybe_filter_no_atps ctxt

          end)

          end)

       |> maybe_instantiate_inducts ctxt hyp_ts concl_t

       |> maybe_instantiate_inducts ctxt hyp_ts concl_t

     end

     end

 end;

 end;