# HG changeset patch
# User bulwahn
# Date 1352400917 -3600
# Node ID c78f9cddc907995171f11f96927718ac0aedde3e
# Parent  a439a9d14ba35231264a374549325c5be5d35864
rewriting with the simpset that is passed to the simproc

diff -r a439a9d14ba3 -r c78f9cddc907 src/HOL/Tools/set_comprehension_pointfree.ML
--- a/src/HOL/Tools/set_comprehension_pointfree.ML	Thu Nov 08 17:11:04 2012 +0100
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Thu Nov 08 19:55:17 2012 +0100
@@ -523,11 +523,14 @@
 
 fun code_simproc ss redex =
   let
-    val prep_thm = Raw_Simplifier.rewrite false @{thms eq_equal[symmetric]} redex
+    fun unfold_conv thms =
+      Raw_Simplifier.rewrite_cterm (false, false, false) (K (K NONE))
+        (Raw_Simplifier.inherit_context ss empty_ss addsimps thms)
+    val prep_thm = unfold_conv @{thms eq_equal[symmetric]} redex
   in
     case base_simproc ss (Thm.rhs_of prep_thm) of
       SOME rewr_thm => SOME (transitive_thm OF [transitive_thm OF [prep_thm, rewr_thm],
-        Raw_Simplifier.rewrite false @{thms eq_equal} (Thm.rhs_of rewr_thm)])
+        unfold_conv @{thms eq_equal} (Thm.rhs_of rewr_thm)])
     | NONE => NONE
   end;