equal
deleted
inserted
replaced
800 "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths)) |
800 "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths)) |
801 in |
801 in |
802 if exists_type type_has_top_sort (prop_of st0) then |
802 if exists_type type_has_top_sort (prop_of st0) then |
803 (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty) |
803 (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty) |
804 else |
804 else |
805 Meson.MESON (K all_tac) (* FIXME: Try (cnf.cnfx_rewrite_tac ctxt) *) |
805 Meson.MESON (K all_tac) (* TODO: Try (cnf.cnfx_rewrite_tac ctxt) *) |
806 (maps neg_clausify) |
806 (maps neg_clausify) |
807 (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) |
807 (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) |
808 ctxt i st0 |
808 ctxt i st0 |
809 end |
809 end |
810 |
810 |