<div dir="ltr"><br><div class="gmail_extra"><br><div class="gmail_quote">On Sat, Jul 18, 2015 at 2:24 PM, Larry Paulson <span dir="ltr"><<a href="mailto:lp15@cam.ac.uk" target="_blank">lp15@cam.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I’ve seen this error consistently in the past week or so. Updating today didn’t help.<br>
<br>
"remote_vampire": Internal error:<br>
exception Match raised (line 407 of "~~/src/HOL/Tools/ATP/atp_proof.ML”)<br></blockquote><div><br></div><div>For what it's worth, I get this too on Isabelle2015 (plus one change to point it at the new URL). </div><div><br></div><div>Maybe it's something on the remote end?</div><div><br></div><div><br></div></div></div></div>