diff -r 1d12e22e7caf -r 7292a7258750 src/HOL/Tools/SMT2/z3_new_replay_methods.ML
--- a/src/HOL/Tools/SMT2/z3_new_replay_methods.ML	Sat May 31 22:31:03 2014 +0200
+++ b/src/HOL/Tools/SMT2/z3_new_replay_methods.ML	Sat May 31 22:59:54 2014 +0200
@@ -435,7 +435,7 @@
 
 fun prove_prop_rewrite ctxt t =
   prove_abstract' ctxt t prop_tac (
-    abstract_eq (abstract_eq abstract_prop) (dest_prop t))
+    abstract_eq abstract_prop (dest_prop t))
 
 fun arith_rewrite_tac ctxt _ =
   TRY o Simplifier.simp_tac ctxt