# HG changeset patch
# User boehmes
# Date 1525070977 -7200
# Node ID 7811d8828775f7c8d6b84d93e5ef4f9eb39b1a90
# Parent  9e077a90520957bfeeacdedbff1bed13b6ba8c7d
prefer explicit error message to unspecific Options exception: Z3 proof traces may lack information necessary for replay when dealing with quantified formulas

diff -r 9e077a905209 -r 7811d8828775 src/HOL/Tools/SMT/z3_proof.ML
--- a/src/HOL/Tools/SMT/z3_proof.ML	Sun Apr 29 21:26:57 2018 +0100
+++ b/src/HOL/Tools/SMT/z3_proof.ML	Mon Apr 30 08:49:37 2018 +0200
@@ -216,9 +216,15 @@
   let
     val match = Sign.typ_match (Proof_Context.theory_of ctxt)
 
+    fun objT_of bound =
+      (case Symtab.lookup env bound of
+        SOME objT => objT
+      | NONE => raise Fail ("Replaying the proof trace produced by Z3 failed: " ^
+          "the bound " ^ quote bound ^ " is undeclared; this indicates a bug in Z3"))
+
     val t' = singleton (Variable.polymorphic ctxt) t
     val patTs = map snd (Term.strip_qnt_vars @{const_name Pure.all} t')
-    val objTs = map (the o Symtab.lookup env) bounds
+    val objTs = map objT_of bounds
     val subst = subst_of (fold match (patTs ~~ objTs) Vartab.empty)
   in Same.commit (Term_Subst.map_types_same (substTs_same subst)) t' end