src/Pure/Isar/proof.ML

     |> int ? (fn goal_state =>
       (case test_proof goal_state of
         Exn.Result (SOME _) => goal_state
       | Exn.Result NONE => error (fail_msg (context_of goal_state))
       | Exn.Exn Exn.Interrupt => raise Exn.Interrupt
-      | Exn.Exn exn => raise Exn.EXCEPTIONS ([exn], fail_msg (context_of goal_state))))
+      | Exn.Exn exn => raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))])))
   end;
 
 in
 
 val have = gen_have Attrib.attribute ProofContext.bind_propp;