src/Pure/par_tactical.ML

--- a/src/Pure/par_tactical.ML	Sat Apr 22 20:55:05 2023 +0200
+++ b/src/Pure/par_tactical.ML	Sat Apr 22 21:00:24 2023 +0200
@@ -59,10 +59,7 @@
     SOME goals =>
       if Future.relevant goals then
         let
-          fun try_goal g =
-            (case SINGLE tac (Goal.init g) of
-              NONE => raise FAILED ()
-            | SOME st' => st');
+          fun try_goal g = SINGLE tac (Goal.init g) |> \<^if_none>\<open>raise FAILED ()\<close>;
           val results = Par_List.map try_goal goals;
         in retrofit_tac {close = false} (rev results) st end handle FAILED () => Seq.empty
       else DETERM tac st