[isabelle-dev] Sledgehammer error involving Vampire

[Jason Dagit]

On Sat, Jul 18, 2015 at 2:24 PM, Larry Paulson <lp15 at cam.ac.uk> wrote:

> I’ve seen this error consistently in the past week or so. Updating today
> didn’t help.
>
> "remote_vampire": Internal error:
> exception Match raised (line 407 of "~~/src/HOL/Tools/ATP/atp_proof.ML”)
>

For what it's worth, I get this too on Isabelle2015 (plus one change to
point it at the new URL).

Maybe it's something on the remote end?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150718/d899d420/attachment-0002.html>