# 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