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.
handling x : S y pattern with the default mechanism instead of raising an exception in the set_comprehension_pointfree simproc
authorbulwahn
Thu, 08 Nov 2012 17:11:04 +0100
changeset 50032 a439a9d14ba3
parent 50031 d12b3a270a62
child 50033 c78f9cddc907
handling x : S y pattern with the default mechanism instead of raising an exception in the set_comprehension_pointfree simproc
src/HOL/Tools/set_comprehension_pointfree.ML file | annotate | diff | comparison | revisions 
--- 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))
isabelle