another refinement in the comprehension conversion
authorbulwahn
Sun Oct 21 08:39:41 2012 +0200 (2012-10-21)
changeset 499590058298658d9
parent 49958 46711464de50
child 49960 1167c1157a5b
another refinement in the comprehension conversion
src/HOL/Tools/set_comprehension_pointfree.ML
     1.1 --- a/src/HOL/Tools/set_comprehension_pointfree.ML	Sun Oct 21 05:24:59 2012 +0200
     1.2 +++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Sun Oct 21 08:39:41 2012 +0200
     1.3 @@ -349,7 +349,7 @@
     1.4      THEN' Subgoal.FOCUS (fn {prems, ...} =>
     1.5        Simplifier.simp_tac
     1.6          (Simplifier.inherit_context ss (HOL_basic_ss addsimps (filter is_eq prems))) 1) ctxt
     1.7 -    THEN' atac
     1.8 +    THEN' TRY o atac
     1.9  in
    1.10    case try mk_term (term_of ct) of
    1.11      NONE => Thm.reflexive ct