src/HOL/Tools/try0.ML

--- a/src/HOL/Tools/try0.ML	Sat Dec 12 15:37:42 2015 +0100
+++ b/src/HOL/Tools/try0.ML	Sun Dec 13 21:56:15 2015 +0100
@@ -70,7 +70,8 @@
         ((name ^ attrs |> attrs <> "" ? enclose "(" ")") ^
          (if all_goals andalso Thm.nprems_of (#goal (Proof.goal st)) > 1 then "[1]" else ""))
         I (#goal o Proof.goal)
-        (apply_named_method_on_first_goal (Proof.context_of st) (name ^ attrs)) st
+        (apply_named_method_on_first_goal (Proof.context_of st) (name ^ attrs)
+          #> Seq.filter_results) st
     end
   else
     NONE;