# 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);