# HG changeset patch
# User wenzelm
# Date 1524659156 -7200
#      Wed Apr 25 14:25:56 2018 +0200
# Node ID 75cc1af8c617d3bb47537366021d3dfbbe2bce65
# Parent  4c9e79aeadf0b5b5d5e5051099f293319e7bbc14
debug

diff -r 4c9e79aeadf0 -r 75cc1af8c617 src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Wed Apr 25 14:13:44 2018 +0200
+++ b/src/HOL/SMT.thy	Wed Apr 25 14:25:56 2018 +0200
@@ -203,7 +203,7 @@
 ML_file "Tools/SMT/smtlib_interface.ML"
 ML_file "Tools/SMT/smtlib_proof.ML"
 ML_file "Tools/SMT/smtlib_isar.ML"
-ML_file "Tools/SMT/z3_proof.ML"
+ML_file_debug "Tools/SMT/z3_proof.ML"
 ML_file "Tools/SMT/z3_isar.ML"
 ML_file "Tools/SMT/smt_solver.ML"
 ML_file "Tools/SMT/cvc4_interface.ML"
diff -r 4c9e79aeadf0 -r 75cc1af8c617 src/HOL/Tools/SMT/z3_proof.ML
--- a/src/HOL/Tools/SMT/z3_proof.ML	Wed Apr 25 14:13:44 2018 +0200
+++ b/src/HOL/Tools/SMT/z3_proof.ML	Wed Apr 25 14:25:56 2018 +0200
@@ -218,7 +218,9 @@
 
     val t' = singleton (Variable.polymorphic ctxt) t
     val patTs = map snd (Term.strip_qnt_vars @{const_name Pure.all} t')
+    val _ = @{print} {t = t, t' = t', patTs = patTs, bounds = bounds, env = env}
     val objTs = map (the o Symtab.lookup env) bounds
+    val _ = @{print} {objTs = objTs}
     val subst = subst_of (fold match (patTs ~~ objTs) Vartab.empty)
   in Same.commit (Term_Subst.map_types_same (substTs_same subst)) t' end