# HG changeset patch
# User wenzelm
# Date 1201215078 -3600
# Node ID 2cfb703fa8d8eade3bceaf16f72d6625b5d53ee6
# Parent  dae57244f1c7f32e8e6a034c76121c01a292b246
improved apply: handle thread position, apply to context here;
replaced ContextPosition by Position.thread_position;

diff -r dae57244f1c7 -r 2cfb703fa8d8 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Thu Jan 24 23:51:17 2008 +0100
+++ b/src/Pure/Isar/method.ML	Thu Jan 24 23:51:18 2008 +0100
@@ -17,7 +17,7 @@
 signature METHOD =
 sig
   include BASIC_METHOD
-  val apply: method -> thm list -> cases_tactic
+  val apply: Position.T -> (Proof.context -> method) -> Proof.context -> thm list -> cases_tactic
   val RAW_METHOD_CASES: (thm list -> cases_tactic) -> method
   val RAW_METHOD: (thm list -> tactic) -> method
   val METHOD_CASES: (thm list -> cases_tactic) -> method
@@ -133,7 +133,8 @@
 
 datatype method = Meth of thm list -> cases_tactic;
 
-fun apply (Meth m) = m;
+fun apply pos meth_fun ctxt facts goal = Position.setmp_thread_data_seq pos
+  (fn () => let val Meth meth = meth_fun ctxt in meth facts goal end) ();
 
 val RAW_METHOD_CASES = Meth;
 
@@ -219,14 +220,15 @@
   if cond (Logic.strip_assums_concl prop)
   then Tactic.rtac rule i else no_tac);
 
-fun legacy_tac ctxt st =
-  (legacy_feature ("implicit use of prems in assumption proof" ^ ContextPosition.str_of ctxt);
+fun legacy_tac st =
+  (legacy_feature
+      ("implicit use of prems in assumption proof" ^ Position.str_of (Position.thread_data ()));
     all_tac st);
 
 fun assm_tac ctxt =
   assume_tac APPEND'
   Goal.assume_rule_tac ctxt APPEND'
-  (CHANGED o solve_tac (Assumption.prems_of ctxt) THEN' K (legacy_tac ctxt)) APPEND'
+  (CHANGED o solve_tac (Assumption.prems_of ctxt) THEN' K legacy_tac) APPEND'
   cond_rtac (can Logic.dest_equals) Drule.reflexive_thm APPEND'
   cond_rtac (can Logic.dest_term) Drule.termI;