src/Pure/Isar/method.ML

   val multi_resolves: thm list -> thm list -> thm Seq.seq
   val rule_tac: thm list -> thm list -> int -> tactic
   val erule_tac: thm list -> thm list -> int -> tactic
   val rule: thm list -> Proof.method
   val erule: thm list -> Proof.method
+  val this: Proof.method
   val assumption: Proof.context -> Proof.method
   exception METHOD_FAIL of (string * Position.T) * exn
   val help_methods: theory option -> unit
   val method: theory -> Args.src -> Proof.context -> Proof.method
   val add_methods: (bstring * (Args.src -> Proof.context -> Proof.method) * string) list

 val some_erule = gen_rule' erule_tac;
 
 end;
 
 
-(* assumption / finish *)
+(* this *)
+
+val this = METHOD (EVERY o map (FINDGOAL o Tactic.rtac));
+
+
+(* assumption *)
 
 fun assm_tac ctxt =
   assume_tac APPEND' resolve_tac (filter Thm.no_prems (ProofContext.prems_of ctxt));
 
 fun assumption_tac ctxt [] = assm_tac ctxt
   | assumption_tac _ [fact] = resolve_tac [fact]
   | assumption_tac _ _ = K no_tac;
 
 fun assumption ctxt = METHOD (FINDGOAL o assumption_tac ctxt);
-fun finish ctxt = METHOD (K (FILTER Thm.no_prems (ALLGOALS (assm_tac ctxt) THEN flexflex_tac)));
 
 
 
 (** methods theory data **)
 

 
 
 (* structured proof steps *)
 
 val default_text = Source (Args.src (("default", []), Position.none));
+val this_text = Basic (K this);
+
+fun finish ctxt = METHOD (K (FILTER Thm.no_prems (ALLGOALS (assm_tac ctxt) THEN flexflex_tac)));
 
 fun finish_text None = Basic finish
   | finish_text (Some txt) = Then [txt, Basic finish];
 
 fun proof opt_text state =

   |> refine (if_none opt_text default_text)
   |> Seq.map Proof.enter_forward;
 
 fun local_qed opt_text = Proof.local_qed (refine (finish_text opt_text));
 fun local_terminal_proof (text, opt_text) pr = Seq.THEN (proof (Some text), local_qed opt_text pr);
-val local_immediate_proof = local_terminal_proof (Basic assumption, None);
+val local_immediate_proof = local_terminal_proof (this_text, None);
 val local_default_proof = local_terminal_proof (default_text, None);
 
 
 fun global_qeds opt_text = Proof.global_qed (refine (finish_text opt_text));
 

   |> Proof.check_result "Terminal proof method failed" state
   |> (Seq.flat o Seq.map (global_qeds opt_text))
   |> Proof.check_result "Failed to finish proof (after successful terminal method)" state
   |> Seq.hd;
 
-val global_immediate_proof = global_terminal_proof (Basic assumption, None);
+val global_immediate_proof = global_terminal_proof (this_text, None);
 val global_default_proof = global_terminal_proof (default_text, None);
 
 
 
 (** theory setup **)

   ("unfold", thms_args unfold, "unfold definitions"),
   ("fold", thms_args fold, "fold definitions"),
   ("default", thms_ctxt_args some_rule, "apply some rule"),
   ("rule", thms_ctxt_args some_rule, "apply some rule"),
   ("erule", thms_ctxt_args some_erule, "apply some erule (improper!)"),
+  ("this", no_args this, "apply current facts as rules"),
   ("assumption", ctxt_args assumption, "proof by assumption, preferring facts")];
 
 
 (* setup *)