equal
deleted
inserted
replaced
629 (*transform isabelle clause to metis clause *) |
629 (*transform isabelle clause to metis clause *) |
630 fun add_thm is_conjecture (ith, {axioms, tfrees}) : logic_map = |
630 fun add_thm is_conjecture (ith, {axioms, tfrees}) : logic_map = |
631 let val (mth, tfree_lits) = hol_thm_to_fol is_conjecture ctxt mode ith |
631 let val (mth, tfree_lits) = hol_thm_to_fol is_conjecture ctxt mode ith |
632 in |
632 in |
633 {axioms = (mth, Meson.make_meta_clause ith) :: axioms, |
633 {axioms = (mth, Meson.make_meta_clause ith) :: axioms, |
634 tfrees = tfree_lits union tfrees} |
634 tfrees = union (op =) (tfree_lits, tfrees)} |
635 end; |
635 end; |
636 val lmap0 = List.foldl (add_thm true) |
636 val lmap0 = List.foldl (add_thm true) |
637 {axioms = [], tfrees = init_tfrees ctxt} cls |
637 {axioms = [], tfrees = init_tfrees ctxt} cls |
638 val lmap = List.foldl (add_thm false) (add_tfrees lmap0) ths |
638 val lmap = List.foldl (add_thm false) (add_tfrees lmap0) ths |
639 val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap) |
639 val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap) |