# HG changeset patch
# User paulson
# Date 1525122801 -3600
# Node ID 6f7829c14f5a41d49e850180c0b6467e179e7901
# Parent  7811d8828775f7c8d6b84d93e5ef4f9eb39b1a90# Parent  69715dfdc2863237e4452856ba62b629fe98fb40
merged

diff -r 69715dfdc286 -r 6f7829c14f5a src/HOL/Tools/SMT/z3_proof.ML
--- a/src/HOL/Tools/SMT/z3_proof.ML	Mon Apr 30 22:13:04 2018 +0100
+++ b/src/HOL/Tools/SMT/z3_proof.ML	Mon Apr 30 22:13:21 2018 +0100
@@ -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