744 "Goal::prop=>prop" to avoid assumptions being returned separately. |
744 "Goal::prop=>prop" to avoid assumptions being returned separately. |
745 *) |
745 *) |
746 fun prepare_proof atomic rths chorn = |
746 fun prepare_proof atomic rths chorn = |
747 let val {sign, t=horn,...} = rep_cterm chorn; |
747 let val {sign, t=horn,...} = rep_cterm chorn; |
748 val _ = Term.no_dummy_patterns horn handle TERM (msg, _) => error msg; |
748 val _ = Term.no_dummy_patterns horn handle TERM (msg, _) => error msg; |
749 val (_,As,B) = Logic.strip_horn(horn); |
749 val (As, B) = Logic.strip_horn horn; |
750 val atoms = atomic andalso |
750 val atoms = atomic andalso |
751 forall (fn t => not(Logic.is_implies t orelse Logic.is_all t)) As; |
751 forall (fn t => not(Logic.is_implies t orelse Logic.is_all t)) As; |
752 val (As,B) = if atoms then ([],horn) else (As,B); |
752 val (As,B) = if atoms then ([],horn) else (As,B); |
753 val cAs = map (cterm_of sign) As; |
753 val cAs = map (cterm_of sign) As; |
754 val prems = map (rewrite_rule rths o forall_elim_vars 0 o Thm.assume) cAs; |
754 val prems = map (rewrite_rule rths o forall_elim_vars 0 o Thm.assume) cAs; |