--- 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