basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context;
Method.Basic: no position;

--- a/src/Pure/Isar/method.ML	Sat Jul 25 14:58:45 2009 +0200
+++ b/src/Pure/Isar/method.ML	Sat Jul 25 18:02:43 2009 +0200
@@ -15,7 +15,7 @@
 sig
   include BASIC_METHOD
   type method
-  val apply: Position.T -> (Proof.context -> method) -> Proof.context -> thm list -> cases_tactic
+  val apply: (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
@@ -55,7 +55,7 @@
   val raw_tactic: string * Position.T -> Proof.context -> method
   type src = Args.src
   datatype text =
-    Basic of (Proof.context -> method) * Position.T |
+    Basic of Proof.context -> method |
     Source of src |
     Source_i of src |
     Then of text list |
@@ -69,7 +69,7 @@
   val this_text: text
   val done_text: text
   val sorry_text: bool -> text
-  val finish_text: text option * bool -> Position.T -> text
+  val finish_text: text option * bool -> text
   val print_methods: theory -> unit
   val intern: theory -> xstring -> string
   val defined: theory -> string -> bool
@@ -106,8 +106,7 @@
 
 datatype method = Meth of thm list -> cases_tactic;
 
-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) ();
+fun apply meth ctxt = let val Meth m = meth ctxt in m end;
 
 val RAW_METHOD_CASES = Meth;
 
@@ -297,7 +296,7 @@
 type src = Args.src;
 
 datatype text =
-  Basic of (Proof.context -> method) * Position.T |
+  Basic of Proof.context -> method |
   Source of src |
   Source_i of src |
   Then of text list |
@@ -306,15 +305,15 @@
   Repeat1 of text |
   SelectGoals of int * text;
 
-fun primitive_text r = Basic (K (SIMPLE_METHOD (PRIMITIVE r)), Position.none);
-val succeed_text = Basic (K succeed, Position.none);
+fun primitive_text r = Basic (K (SIMPLE_METHOD (PRIMITIVE r)));
+val succeed_text = Basic (K succeed);
 val default_text = Source (Args.src (("default", []), Position.none));
-val this_text = Basic (K this, Position.none);
-val done_text = Basic (K (SIMPLE_METHOD all_tac), Position.none);
-fun sorry_text int = Basic (cheating int, Position.none);
+val this_text = Basic (K this);
+val done_text = Basic (K (SIMPLE_METHOD all_tac));
+fun sorry_text int = Basic (cheating int);
 
-fun finish_text (NONE, immed) pos = Basic (close immed, pos)
-  | finish_text (SOME txt, immed) pos = Then [txt, Basic (close immed, pos)];
+fun finish_text (NONE, immed) = Basic (close immed)
+  | finish_text (SOME txt, immed) = Then [txt, Basic (close immed)];
 
 
 (* method definitions *)
@@ -477,8 +476,8 @@
 
 end;
 
-structure BasicMethod: BASIC_METHOD = Method;
-open BasicMethod;
+structure Basic_Method: BASIC_METHOD = Method;
+open Basic_Method;
 
 val RAW_METHOD_CASES = Method.RAW_METHOD_CASES;
 val RAW_METHOD = Method.RAW_METHOD;

--- a/src/Pure/Isar/proof.ML	Sat Jul 25 14:58:45 2009 +0200
+++ b/src/Pure/Isar/proof.ML	Sat Jul 25 18:02:43 2009 +0200
@@ -386,13 +386,13 @@
 fun goal_cases st =
   RuleCases.make_common true (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair []) (goals st));
 
-fun apply_method current_context pos meth state =
+fun apply_method current_context meth state =
   let
     val (goal_ctxt, (_, {statement, messages = _, using, goal, before_qed, after_qed})) =
       find_goal state;
     val ctxt = if current_context then context_of state else goal_ctxt;
   in
-    Method.apply pos meth ctxt using goal |> Seq.map (fn (meth_cases, goal') =>
+    Method.apply meth ctxt using goal |> Seq.map (fn (meth_cases, goal') =>
       state
       |> map_goal
           (ProofContext.add_cases false (no_goal_cases goal @ goal_cases goal') #>
@@ -410,16 +410,15 @@
     |> Seq.maps meth
     |> Seq.maps (fn state' => state'
       |> Seq.lift set_goal (Goal.retrofit 1 n (#2 (#2 (get_goal state'))) goal))
-    |> Seq.maps (apply_method true Position.none (K Method.succeed)));
+    |> Seq.maps (apply_method true (K Method.succeed)));
 
 fun apply_text cc text state =
   let
     val thy = theory_of state;
-    val pos_of = #2 o Args.dest_src;
 
-    fun eval (Method.Basic (m, pos)) = apply_method cc pos m
-      | eval (Method.Source src) = apply_method cc (pos_of src) (Method.method thy src)
-      | eval (Method.Source_i src) = apply_method cc (pos_of src) (Method.method_i thy src)
+    fun eval (Method.Basic m) = apply_method cc m
+      | eval (Method.Source src) = apply_method cc (Method.method thy src)
+      | eval (Method.Source_i src) = apply_method cc (Method.method_i thy src)
       | eval (Method.Then txts) = Seq.EVERY (map eval txts)
       | eval (Method.Orelse txts) = Seq.FIRST (map eval txts)
       | eval (Method.Try txt) = Seq.TRY (eval txt)
@@ -433,7 +432,7 @@
 val refine_end = apply_text false;
 
 fun refine_insert [] = I
-  | refine_insert ths = Seq.hd o refine (Method.Basic (K (Method.insert ths), Position.none));
+  | refine_insert ths = Seq.hd o refine (Method.Basic (K (Method.insert ths)));
 
 end;
 
@@ -750,7 +749,7 @@
   |> assert_current_goal true
   |> using_facts []
   |> `before_qed |-> (refine o the_default Method.succeed_text)
-  |> Seq.maps (refine (Method.finish_text txt (Position.thread_data ())));
+  |> Seq.maps (refine (Method.finish_text txt));
 
 fun check_result msg sq =
   (case Seq.pull sq of
@@ -762,8 +761,8 @@
 
 (* unstructured refinement *)
 
-fun defer i = assert_no_chain #> refine (Method.Basic (K (Method.defer i), Position.none));
-fun prefer i = assert_no_chain #> refine (Method.Basic (K (Method.prefer i), Position.none));
+fun defer i = assert_no_chain #> refine (Method.Basic (K (Method.defer i)));
+fun prefer i = assert_no_chain #> refine (Method.Basic (K (Method.prefer i)));
 
 fun apply text = assert_backward #> refine text #> Seq.map (using_facts []);
 fun apply_end text = assert_forward #> refine_end text;
@@ -789,7 +788,7 @@
 fun refine_terms n =
   refine (Method.Basic (K (RAW_METHOD
     (K (HEADGOAL (PRECISE_CONJUNCTS n
-      (HEADGOAL (CONJUNCTS (ALLGOALS (rtac Drule.termI)))))))), Position.none))
+      (HEADGOAL (CONJUNCTS (ALLGOALS (rtac Drule.termI))))))))))
   #> Seq.hd;
 
 in
@@ -832,7 +831,7 @@
     |> put_goal NONE
     |> enter_backward
     |> not (null vars) ? refine_terms (length goal_propss)
-    |> null props ? (refine (Method.Basic (Method.assumption, Position.none)) #> Seq.hd)
+    |> null props ? (refine (Method.Basic Method.assumption) #> Seq.hd)
   end;
 
 fun generic_qed after_ctxt state =