src/HOL/Tools/set_comprehension_pointfree.ML
changeset 49959 0058298658d9
parent 49958 46711464de50
child 50024 b7265db3a1dc
--- 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