be more liberal in reconstructing congruences from Z3 (sometimes the symmetric version of a premise is needed)

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