--- 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