# HG changeset patch
# User wenzelm
# Date 1236121520 -3600
# Node ID 7dd251bce291c69ee877d1d53a03c6075bd7bf50
# Parent  6eb726e43ed1d15fccc14b036fc39442aa2f8db4
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);

diff -r 6eb726e43ed1 -r 7dd251bce291 src/Pure/Isar/method.ML
--- 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;
 
diff -r 6eb726e43ed1 -r 7dd251bce291 src/Pure/Tools/find_theorems.ML
--- 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