[isabelle-dev] Sledgehammer

[Clemens Ballarin]

While doing an 'isabelle makeall all' on my local machine, I  
encountered the error

   Sledgehammering...
   *** Unexpected outcome: "unknown".
   *** At command "sledgehammer" (line 26 of  
"/Users/ballarin/isabelle/hg/src/HOL/Metis_Examples/Proxies.thy")


I guess I lack some sort of heavy equipment here.  What surprises me  
is that on macbroy2 I don't have set up sledgehammer either, but I  
don't get this error.

Clemens