# HG changeset patch
# User boehmes
# Date 1256033177 -7200
# Node ID b73b74fe23c330cb09928d25abcdba92becececd
# Parent  ab599f7f26397212e11995091bffe80c24f4611f
proper exceptions instead of unhandled partiality

diff -r ab599f7f2639 -r b73b74fe23c3 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Oct 20 10:29:47 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Oct 20 12:06:17 2009 +0200
@@ -279,9 +279,18 @@
 
 
 fun get_atp thy args =
-  AList.lookup (op =) args proverK
-  |> the_default (hd (ATP_Manager.get_atps ()))  (* FIXME partial *)
-  |> (fn name => (name, the (ATP_Manager.get_prover thy name)))  (* FIXME partial *)
+  let
+    fun default_atp_name () = hd (ATP_Manager.get_atps ())
+      handle Empty => error "No ATP available."
+    fun get_prover name =
+      (case ATP_Manager.get_prover thy name of
+        SOME prover => (name, prover)
+      | NONE => error ("Bad ATP: " ^ quote name))
+  in
+    (case AList.lookup (op =) args proverK of
+      SOME name => get_prover name
+    | NONE => get_prover (default_atp_name ()))
+  end
 
 local