# HG changeset patch
# User blanchet
# Date 1305206959 -7200
# Node ID 369dfc8190568dd750641764935dbefe38e06023
# Parent  546b0bda3cb838fc915e70c7f594dcb93702f81f
unfold set constants in Sledgehammer/ATP as well if Metis does it too

diff -r 546b0bda3cb8 -r 369dfc819056 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- 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))