diff -r 484cd3a304a8 -r ec7ca5388dea src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Feb 26 11:14:38 2014 +0100
+++ b/src/Pure/Isar/proof.ML	Wed Feb 26 11:58:35 2014 +0100
@@ -423,11 +423,11 @@
     fun eval (Method.Basic m) = apply_method current_context m
       | eval (Method.Source src) =
           apply_method current_context (Method.the_method ctxt (Method.check_source ctxt 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)
-      | eval (Method.Repeat1 txt) = Seq.REPEAT1 (eval txt)
-      | eval (Method.Select_Goals (n, txt)) = select_goals n (eval txt);
+      | 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)
+      | eval (Method.Repeat1 (_, txt)) = Seq.REPEAT1 (eval txt)
+      | eval (Method.Select_Goals (_, n, txt)) = select_goals n (eval txt);
   in eval text state end;
 
 in