src/Pure/Isar/proof.ML
changeset 55742 a989bdaf8121
parent 55709 4e5a83a46ded
child 55765 ec7ca5388dea
     1.1 --- a/src/Pure/Isar/proof.ML	Tue Feb 25 12:53:08 2014 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Tue Feb 25 14:34:18 2014 +0100
     1.3 @@ -392,13 +392,13 @@
     1.4    Rule_Cases.make_common
     1.5      (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair [] o rpair []) (goals st));
     1.6  
     1.7 -fun apply_method current_context meth state =
     1.8 +fun apply_method current_context method 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 meth ctxt using goal |> Seq.map (fn (meth_cases, goal') =>
    1.15 +    Method.apply method ctxt using goal |> Seq.map (fn (meth_cases, goal') =>
    1.16        state
    1.17        |> map_goal
    1.18            (Proof_Context.update_cases false (no_goal_cases goal @ goal_cases goal') #>
    1.19 @@ -416,13 +416,13 @@
    1.20        |> Seq.lift provide_goal (PRIMITIVE (Goal.unrestrict 1) (#2 (#2 (get_goal state')))))
    1.21      |> Seq.maps (apply_method true (K Method.succeed)));
    1.22  
    1.23 -fun apply_text cc text state =
    1.24 +fun apply_text current_context text state =
    1.25    let
    1.26 -    val thy = theory_of state;
    1.27 +    val ctxt = context_of state;
    1.28  
    1.29 -    fun eval (Method.Basic m) = apply_method cc m
    1.30 -      | eval (Method.Source src) = apply_method cc (Method.method thy src)
    1.31 -      | eval (Method.Source_i src) = apply_method cc (Method.method_i thy src)
    1.32 +    fun eval (Method.Basic m) = apply_method current_context m
    1.33 +      | eval (Method.Source src) =
    1.34 +          apply_method current_context (Method.the_method ctxt (Method.check_source ctxt src))
    1.35        | eval (Method.Then txts) = Seq.EVERY (map eval txts)
    1.36        | eval (Method.Orelse txts) = Seq.FIRST (map eval txts)
    1.37        | eval (Method.Try txt) = Seq.TRY (eval txt)