1057 val tprems = map term_of prems; |
1057 val tprems = map term_of prems; |
1058 val i = 1 + Library.foldl Int.max (~1, map (fn p => |
1058 val i = 1 + Library.foldl Int.max (~1, map (fn p => |
1059 find_index_eq p tprems) (#hyps (rep_thm eqn))); |
1059 find_index_eq p tprems) (#hyps (rep_thm eqn))); |
1060 val (rrs', asm') = rules_of_prem ss prem' |
1060 val (rrs', asm') = rules_of_prem ss prem' |
1061 in mut_impc prems concl rrss asms (prem' :: prems') |
1061 in mut_impc prems concl rrss asms (prem' :: prems') |
1062 (rrs' :: rrss') (asm' :: asms') (SOME (Library.foldr (disch true) |
1062 (rrs' :: rrss') (asm' :: asms') (SOME (foldr (disch true) |
1063 (Library.take (i, prems), Drule.imp_cong' eqn (reflexive (Drule.list_implies |
1063 (Drule.imp_cong' eqn (reflexive (Drule.list_implies |
1064 (Library.drop (i, prems), concl))))) :: eqns) ss (length prems') ~1 |
1064 (Library.drop (i, prems), concl)))) (Library.take (i, prems))) :: eqns) ss (length prems') ~1 |
1065 end |
1065 end |
1066 |
1066 |
1067 (*legacy code - only for backwards compatibility*) |
1067 (*legacy code - only for backwards compatibility*) |
1068 and nonmut_impc ct ss = |
1068 and nonmut_impc ct ss = |
1069 let val (prem, conc) = dest_implies ct; |
1069 let val (prem, conc) = dest_implies ct; |