equal
deleted
inserted
replaced
474 val newhyps = filter_out (member (op aconv) hyps0 o Thm.term_of) hyps |
474 val newhyps = filter_out (member (op aconv) hyps0 o Thm.term_of) hyps |
475 val defs = filter (is_absko o Thm.term_of) newhyps |
475 val defs = filter (is_absko o Thm.term_of) newhyps |
476 val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs)) |
476 val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs)) |
477 (map Thm.term_of hyps) |
477 (map Thm.term_of hyps) |
478 val fixed = OldTerm.term_frees (concl_of st) @ |
478 val fixed = OldTerm.term_frees (concl_of st) @ |
479 List.foldl (gen_union (op aconv)) [] (map OldTerm.term_frees remaining_hyps) |
479 List.foldl (union (op aconv)) [] (map OldTerm.term_frees remaining_hyps) |
480 in Seq.of_list [LocalDefs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end; |
480 in Seq.of_list [LocalDefs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end; |
481 |
481 |
482 |
482 |
483 fun meson_general_tac ctxt ths i st0 = |
483 fun meson_general_tac ctxt ths i st0 = |
484 let |
484 let |