renamed Method.assumption_tac back to Method.assm_tac -- as assumption_tac it would have to be exactly the tactic behind the assumption method (with facts);
--- a/src/Pure/Isar/method.ML Tue Mar 03 21:53:52 2009 +0100
+++ b/src/Pure/Isar/method.ML Wed Mar 04 00:05:20 2009 +0100
@@ -38,7 +38,7 @@
val atomize: bool -> method
val this: method
val fact: thm list -> Proof.context -> method
- val assumption_tac: Proof.context -> int -> tactic
+ val assm_tac: Proof.context -> int -> tactic
val assumption: Proof.context -> method
val close: bool -> Proof.context -> method
val trace: Proof.context -> thm list -> unit
@@ -224,20 +224,20 @@
in
-fun assumption_tac ctxt =
+fun assm_tac ctxt =
assume_tac APPEND'
Goal.assume_rule_tac ctxt APPEND'
cond_rtac (can Logic.dest_equals) Drule.reflexive_thm APPEND'
cond_rtac (can Logic.dest_term) Drule.termI;
fun assumption ctxt = METHOD (HEADGOAL o
- (fn [] => assumption_tac ctxt
+ (fn [] => assm_tac ctxt
| [fact] => solve_tac [fact]
| _ => K no_tac));
fun close immed ctxt = METHOD (K
(FILTER Thm.no_prems
- ((if immed then ALLGOALS (assumption_tac ctxt) else all_tac) THEN flexflex_tac)));
+ ((if immed then ALLGOALS (assm_tac ctxt) else all_tac) THEN flexflex_tac)));
end;
--- a/src/Pure/Tools/find_theorems.ML Tue Mar 03 21:53:52 2009 +0100
+++ b/src/Pure/Tools/find_theorems.ML Wed Mar 04 00:05:20 2009 +0100
@@ -169,8 +169,7 @@
fun try_thm thm =
if Thm.no_prems thm then rtac thm 1 goal
else (etacn thm THEN_ALL_NEW
- (Goal.norm_hhf_tac THEN'
- Method.assumption_tac ctxt)) 1 goal;
+ (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt)) 1 goal;
in
fn (_, thm) =>
if (is_some o Seq.pull o try_thm) thm