# HG changeset patch
# User bulwahn
# Date 1350789899 -7200
# Node ID 46711464de507254d3a16d5cc858473cd9d236e4
# Parent  6250121bfffb7af74bd0cfd8834fff444b9b07f8
refined simplifier call in comprehension_conv

diff -r 6250121bfffb -r 46711464de50 src/HOL/Tools/set_comprehension_pointfree.ML
--- a/src/HOL/Tools/set_comprehension_pointfree.ML	Sun Oct 21 05:24:56 2012 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Sun Oct 21 05:24:59 2012 +0200
@@ -335,6 +335,7 @@
       HOLogic.Collect_const T $ absdummy T (list_ex vs (HOLogic.mk_conj (eq, t'')))
     end;
   val unfold_thms = @{thms split_paired_all mem_Collect_eq prod.cases}
+  fun is_eq th = is_some (try (HOLogic.dest_eq o HOLogic.dest_Trueprop) (prop_of th))
   fun tac ctxt = 
     rtac @{thm set_eqI}
     THEN' Simplifier.simp_tac
@@ -346,7 +347,9 @@
     THEN' etac @{thm conjE}
     THEN' REPEAT_DETERM o etac @{thm Pair_inject}
     THEN' Subgoal.FOCUS (fn {prems, ...} =>
-      Simplifier.full_simp_tac (Simplifier.inherit_context ss (HOL_ss addsimps prems)) 1) ctxt
+      Simplifier.simp_tac
+        (Simplifier.inherit_context ss (HOL_basic_ss addsimps (filter is_eq prems))) 1) ctxt
+    THEN' atac
 in
   case try mk_term (term_of ct) of
     NONE => Thm.reflexive ct