# HG changeset patch
# User boehmes
# Date 1290585108 -3600
# Node ID 02caa72cb95029830ea17b6774ee933c6738ef91
# Parent  f3f088322a7776083f8b851d042c449b7f5ab11f
be more liberal in reconstructing congruences from Z3 (sometimes the symmetric version of a premise is needed)

diff -r f3f088322a77 -r 02caa72cb950 src/HOL/Tools/SMT/z3_proof_reconstruction.ML
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Tue Nov 23 23:44:11 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Wed Nov 24 08:51:48 2010 +0100
@@ -486,7 +486,9 @@
 in
 fun monotonicity eqs ct =
   let
-    val lookup = AList.lookup (op aconv) (map (`Thm.prop_of o meta_eq_of) eqs)
+    fun and_symmetric (t, thm) = [(t, thm), (t, Thm.symmetric thm)]
+    val teqs = maps (and_symmetric o `Thm.prop_of o meta_eq_of) eqs
+    val lookup = AList.lookup (op aconv) teqs
     val cp = Thm.dest_binop (Thm.dest_arg ct)
   in MetaEq (prove_eq_exn lookup cp handle MONO => mono lookup cp) end
 end