1.1 --- a/src/Pure/Isar/proof.ML	Sat Jul 25 14:58:45 2009 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Sat Jul 25 18:02:43 2009 +0200
     1.3 @@ -386,13 +386,13 @@
     1.4  fun goal_cases st =
     1.5    RuleCases.make_common true (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair []) (goals st));
     1.6  
     1.7 -fun apply_method current_context pos meth state =
     1.8 +fun apply_method current_context meth state =
     1.9    let
    1.10      val (goal_ctxt, (_, {statement, messages = _, using, goal, before_qed, after_qed})) =
    1.11        find_goal state;
    1.12      val ctxt = if current_context then context_of state else goal_ctxt;
    1.13    in
    1.14 -    Method.apply pos meth ctxt using goal |> Seq.map (fn (meth_cases, goal') =>
    1.15 +    Method.apply meth ctxt using goal |> Seq.map (fn (meth_cases, goal') =>
    1.16        state
    1.17        |> map_goal
    1.18            (ProofContext.add_cases false (no_goal_cases goal @ goal_cases goal') #>
    1.19 @@ -410,16 +410,15 @@
    1.20      |> Seq.maps meth
    1.21      |> Seq.maps (fn state' => state'
    1.22        |> Seq.lift set_goal (Goal.retrofit 1 n (#2 (#2 (get_goal state'))) goal))
    1.23 -    |> Seq.maps (apply_method true Position.none (K Method.succeed)));
    1.24 +    |> Seq.maps (apply_method true (K Method.succeed)));
    1.25  
    1.26  fun apply_text cc text state =
    1.27    let
    1.28      val thy = theory_of state;
    1.29 -    val pos_of = #2 o Args.dest_src;
    1.30  
    1.31 -    fun eval (Method.Basic (m, pos)) = apply_method cc pos m
    1.32 -      | eval (Method.Source src) = apply_method cc (pos_of src) (Method.method thy src)
    1.33 -      | eval (Method.Source_i src) = apply_method cc (pos_of src) (Method.method_i thy src)
    1.34 +    fun eval (Method.Basic m) = apply_method cc m
    1.35 +      | eval (Method.Source src) = apply_method cc (Method.method thy src)
    1.36 +      | eval (Method.Source_i src) = apply_method cc (Method.method_i thy src)
    1.37        | eval (Method.Then txts) = Seq.EVERY (map eval txts)
    1.38        | eval (Method.Orelse txts) = Seq.FIRST (map eval txts)
    1.39        | eval (Method.Try txt) = Seq.TRY (eval txt)
    1.40 @@ -433,7 +432,7 @@
    1.41  val refine_end = apply_text false;
    1.42  
    1.43  fun refine_insert [] = I
    1.44 -  | refine_insert ths = Seq.hd o refine (Method.Basic (K (Method.insert ths), Position.none));
    1.45 +  | refine_insert ths = Seq.hd o refine (Method.Basic (K (Method.insert ths)));
    1.46  
    1.47  end;
    1.48  
    1.49 @@ -750,7 +749,7 @@
    1.50    |> assert_current_goal true
    1.51    |> using_facts []
    1.52    |> `before_qed |-> (refine o the_default Method.succeed_text)
    1.53 -  |> Seq.maps (refine (Method.finish_text txt (Position.thread_data ())));
    1.54 +  |> Seq.maps (refine (Method.finish_text txt));
    1.55  
    1.56  fun check_result msg sq =
    1.57    (case Seq.pull sq of
    1.58 @@ -762,8 +761,8 @@
    1.59  
    1.60  (* unstructured refinement *)
    1.61  
    1.62 -fun defer i = assert_no_chain #> refine (Method.Basic (K (Method.defer i), Position.none));
    1.63 -fun prefer i = assert_no_chain #> refine (Method.Basic (K (Method.prefer i), Position.none));
    1.64 +fun defer i = assert_no_chain #> refine (Method.Basic (K (Method.defer i)));
    1.65 +fun prefer i = assert_no_chain #> refine (Method.Basic (K (Method.prefer i)));
    1.66  
    1.67  fun apply text = assert_backward #> refine text #> Seq.map (using_facts []);
    1.68  fun apply_end text = assert_forward #> refine_end text;
    1.69 @@ -789,7 +788,7 @@
    1.70  fun refine_terms n =
    1.71    refine (Method.Basic (K (RAW_METHOD
    1.72      (K (HEADGOAL (PRECISE_CONJUNCTS n
    1.73 -      (HEADGOAL (CONJUNCTS (ALLGOALS (rtac Drule.termI)))))))), Position.none))
    1.74 +      (HEADGOAL (CONJUNCTS (ALLGOALS (rtac Drule.termI))))))))))
    1.75    #> Seq.hd;
    1.76  
    1.77  in
    1.78 @@ -832,7 +831,7 @@
    1.79      |> put_goal NONE
    1.80      |> enter_backward
    1.81      |> not (null vars) ? refine_terms (length goal_propss)
    1.82 -    |> null props ? (refine (Method.Basic (Method.assumption, Position.none)) #> Seq.hd)
    1.83 +    |> null props ? (refine (Method.Basic Method.assumption) #> Seq.hd)
    1.84    end;
    1.85  
    1.86  fun generic_qed after_ctxt state =