# HG changeset patch
# User bulwahn
# Date 1350801581 -7200
# Node ID 0058298658d93b935500a4931087fa3262840a2a
# Parent  46711464de507254d3a16d5cc858473cd9d236e4
another refinement in the comprehension conversion

diff -r 46711464de50 -r 0058298658d9 src/HOL/Tools/set_comprehension_pointfree.ML
--- a/src/HOL/Tools/set_comprehension_pointfree.ML	Sun Oct 21 05:24:59 2012 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Sun Oct 21 08:39:41 2012 +0200
@@ -349,7 +349,7 @@
     THEN' Subgoal.FOCUS (fn {prems, ...} =>
       Simplifier.simp_tac
         (Simplifier.inherit_context ss (HOL_basic_ss addsimps (filter is_eq prems))) 1) ctxt
-    THEN' atac
+    THEN' TRY o atac
 in
   case try mk_term (term_of ct) of
     NONE => Thm.reflexive ct