unfold set constants in Sledgehammer/ATP as well if Metis does it too

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 12 15:29:19 2011 +0200
@@ -434,6 +434,8 @@
               |> Object_Logic.atomize_term thy
     val need_trueprop = (fastype_of t = @{typ bool})
     val t = t |> need_trueprop ? HOLogic.mk_Trueprop
+              |> Raw_Simplifier.rewrite_term thy
+                     (Meson.unfold_set_const_simps ctxt) []
               |> extensionalize_term
               |> presimp ? presimplify_term thy
               |> perhaps (try (HOLogic.dest_Trueprop))