# HG changeset patch
# User blanchet
# Date 1494436618 -7200
# Node ID aeb776b5b0546851c6ef4d502f8beb4b1d091c49
# Parent  d53be22028599c14e3219ac23e1c40b61e334a35
made SMT reconstruction more complete (bug report by Lukas Bulwahn)

diff -r d53be2202859 -r aeb776b5b054 src/HOL/Tools/SMT/z3_replay_methods.ML
--- a/src/HOL/Tools/SMT/z3_replay_methods.ML	Wed May 10 19:11:20 2017 +0200
+++ b/src/HOL/Tools/SMT/z3_replay_methods.ML	Wed May 10 19:16:58 2017 +0200
@@ -323,11 +323,16 @@
   "(P | ~ Q) & (~ P | Q) ==> P = Q"
   by fast+}
 
+fun cong_full_core_tac ctxt =
+  eresolve_tac ctxt @{thms subst}
+  THEN' resolve_tac ctxt @{thms refl}
+  ORELSE' Classical.fast_tac ctxt
+
 fun cong_full ctxt thms t = prove ctxt t (fn ctxt' =>
   Method.insert_tac ctxt thms
-  THEN' (Classical.fast_tac ctxt'
+  THEN' (cong_full_core_tac ctxt'
     ORELSE' dresolve_tac ctxt cong_dest_rules
-    THEN' Classical.fast_tac ctxt'))
+    THEN' cong_full_core_tac ctxt'))
 
 fun cong ctxt thms = try_provers ctxt Z3_Proof.Monotonicity [
   ("basic", cong_basic ctxt thms),