src/Pure/Tools/sledgehammer_params.scala
changeset 54442 c39972ddd672
parent 53055 0fe8a9972eda
child 55200 777328c9f1ea
--- a/src/Pure/Tools/sledgehammer_params.scala	Thu Nov 14 17:39:32 2013 +0100
+++ b/src/Pure/Tools/sledgehammer_params.scala	Fri Nov 15 19:31:10 2013 +0100
@@ -37,13 +37,10 @@
     def get_provers: String = synchronized { _provers }
 
     private def sledgehammer_provers(
-      prover: Session.Prover, output: Isabelle_Process.Output): Boolean =
+      prover: Session.Prover, msg: Isabelle_Process.Protocol_Output): Boolean =
     {
-      output.body match {
-        case Nil => update_provers(""); true
-        case List(XML.Text(s)) => update_provers(s); true
-        case _ => false
-      }
+      update_provers(msg.text)
+      true
     }
 
     val functions =