Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
another refinement in the comprehension conversion
authorbulwahn
Sun, 21 Oct 2012 08:39:41 +0200
changeset 49959 0058298658d9
parent 49958 46711464de50
child 49960 1167c1157a5b
another refinement in the comprehension conversion
src/HOL/Tools/set_comprehension_pointfree.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle