# HG changeset patch
# User bulwahn
# Date 1352391064 -3600
# Node ID a439a9d14ba35231264a374549325c5be5d35864
# Parent  d12b3a270a62d68105fb55543310e37ba8c30c4f
handling x : S y pattern with the default mechanism instead of raising an exception in the set_comprehension_pointfree simproc

diff -r d12b3a270a62 -r a439a9d14ba3 src/HOL/Tools/set_comprehension_pointfree.ML
--- a/src/HOL/Tools/set_comprehension_pointfree.ML	Thu Nov 08 17:06:59 2012 +0100
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Thu Nov 08 17:11:04 2012 +0100
@@ -156,9 +156,9 @@
     (tuple, Atom (tuple, s))
   end
 
-fun mk_atom vs (Const (@{const_name "Set.member"}, _) $ x $ s) =
+fun mk_atom vs (t as Const (@{const_name "Set.member"}, _) $ x $ s) =
     if not (null (loose_bnos s)) then
-      raise TERM ("mk_atom: bound variables in the set expression", [s])
+      default_atom vs t
     else
       (case try ((map dest_bound) o HOLogic.strip_tuple) x of
       SOME pat => (Pattern pat, Atom (Pattern pat, s))