diff -r 0ed1e999a0fb -r 250ecd2502ad src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue Aug 19 12:05:11 2014 +0200
+++ b/src/Pure/Isar/method.ML	Tue Aug 19 14:51:25 2014 +0200
@@ -69,6 +69,7 @@
     local_theory -> local_theory
   val method_setup: bstring * Position.T -> Symbol_Pos.source -> string ->
     local_theory -> local_theory
+  val evaluate: Proof.context -> text -> Proof.context -> method
   type modifier = (Proof.context -> Proof.context) * attribute
   val section: modifier parser list -> thm list context_parser
   val sections: modifier parser list -> thm list list context_parser
@@ -389,6 +390,44 @@
   |> Context.proof_map;
 
 
+(* evaluate method text *)
+
+local
+
+fun APPEND_CASES (meth: cases_tactic) (cases, st) =
+  meth st |> Seq.map (fn (cases', st') => (cases @ cases', st'));
+
+fun BYPASS_CASES (tac: tactic) (cases, st) =
+  tac st |> Seq.map (pair cases);
+
+val op THEN = Seq.THEN;
+
+fun SELECT_GOALS n method =
+  BYPASS_CASES
+    (ALLGOALS Goal.conjunction_tac THEN PRIMITIVE (Goal.restrict 1 n) THEN Goal.conjunction_tac 1)
+  THEN method
+  THEN BYPASS_CASES (PRIMITIVE (Goal.unrestrict 1));
+
+fun combinator comb meths ctxt facts = comb (map (fn meth => meth ctxt facts) meths);
+fun combinator1 comb meth ctxt facts = comb (meth ctxt facts);
+
+in
+
+fun evaluate static_ctxt text =
+  let
+    fun eval (Basic meth) = APPEND_CASES oo meth
+      | eval (Source src) = APPEND_CASES oo method_cmd static_ctxt src
+      | eval (Then (_, txts)) = combinator Seq.EVERY (map eval txts)
+      | eval (Orelse (_, txts)) = combinator Seq.FIRST (map eval txts)
+      | eval (Try (_, txt)) = combinator1 Seq.TRY (eval txt)
+      | eval (Repeat1 (_, txt)) = combinator1 Seq.REPEAT1 (eval txt)
+      | eval (Select_Goals (_, n, txt)) = combinator1 (SELECT_GOALS n) (eval txt);
+    val meth = eval text;
+  in fn ctxt => fn facts => fn st => meth ctxt facts ([], st) end;
+
+end;
+
+
 
 (** concrete syntax **)