# HG changeset patch
# User wenzelm
# Date 924877983 -7200
# Node ID 68ba555ac59a5a84538944f754c455fc0a832d4a
# Parent  2fd9124869902eacbb5066eb41aced4c6e50b8cd
added FINISHED, same_tac;

diff -r 2fd912486990 -r 68ba555ac59a src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Fri Apr 23 16:31:12 1999 +0200
+++ b/src/Pure/Isar/method.ML	Fri Apr 23 16:33:03 1999 +0200
@@ -14,11 +14,13 @@
 signature METHOD =
 sig
   include BASIC_METHOD
+  val FINISHED: tactic -> tactic
   val LIFT: tactic -> thm -> (thm * (indexname * term) list * (string * thm list) list) Seq.seq
   val METHOD: (thm list -> tactic) -> Proof.method
   val METHOD0: tactic -> Proof.method
   val fail: Proof.method
   val succeed: Proof.method
+  val same_tac: thm list -> int -> tactic
   val same: Proof.method
   val assumption: Proof.method
   val forward_chain: thm list -> thm list -> thm Seq.seq
@@ -69,6 +71,12 @@
 struct
 
 
+(** utils **)
+
+val FINISHED = FILTER (equal 0 o Thm.nprems_of);
+
+
+
 (** proof methods **)
 
 (* method from tactic *)
@@ -94,7 +102,7 @@
 val same = METHOD (ALLGOALS o same_tac);
 val assumption = METHOD (fn facts => FIRSTGOAL (same_tac facts THEN' assume_tac));
 
-val asm_finish = METHOD (K (FILTER (equal 0 o Thm.nprems_of) (ALLGOALS assume_tac)));
+val asm_finish = METHOD (K (FINISHED (ALLGOALS assume_tac)));
 
 
 (* rule *)