# HG changeset patch # User wenzelm # Date 973283171 -3600 # Node ID 98c95ebf804fa5eaf6071c7d8154dad35e6184c2 # Parent 6b595f9ae37e253504ae95297178733592714d41 assumption / finish: handle non-atomic assumptions from context as well; diff -r 6b595f9ae37e -r 98c95ebf804f src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Fri Nov 03 21:25:30 2000 +0100 +++ b/src/Pure/Isar/method.ML Fri Nov 03 21:26:11 2000 +0100 @@ -356,11 +356,13 @@ (* assumption *) -fun assm_tac ctxt = - assume_tac APPEND' resolve_tac (filter Thm.no_prems (ProofContext.prems_of ctxt)); +fun asm_tac ths = + foldr (op APPEND') (map (fn th => Tactic.rtac th THEN_ALL_NEW assume_tac) ths, K no_tac); + +fun assm_tac ctxt = assume_tac APPEND' asm_tac (ProofContext.prems_of ctxt); fun assumption_tac ctxt [] = assm_tac ctxt - | assumption_tac _ [fact] = resolve_tac [fact] + | assumption_tac _ [fact] = asm_tac [fact] | assumption_tac _ _ = K no_tac; fun assumption ctxt = METHOD (HEADGOAL o assumption_tac ctxt);