# HG changeset patch
# User bulwahn
# Date 1352390819 -3600
# Node ID d12b3a270a62d68105fb55543310e37ba8c30c4f
# Parent  349f651ec2039e5f990386ac80c5cae235a14b4d
tuned

diff -r 349f651ec203 -r d12b3a270a62 src/HOL/Tools/set_comprehension_pointfree.ML
--- a/src/HOL/Tools/set_comprehension_pointfree.ML	Thu Nov 08 16:25:26 2012 +0100
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Thu Nov 08 17:06:59 2012 +0100
@@ -289,7 +289,7 @@
       (0 upto (length vs - 1))
     val (pats, fm) =
       mk_formula ((x, T) :: vs) (foldr1 HOLogic.mk_conj (conjs' @ map mk_mem_UNIV unused_bounds))
-    fun mk_set (Atom pt) = (case map (lookup pt) pats of [t'] => t' | ts => foldr1 mk_sigma ts)
+    fun mk_set (Atom pt) = foldr1 mk_sigma (map (lookup pt) pats)
       | mk_set (Un (f1, f2)) = mk_sup (mk_set f1, mk_set f2)
       | mk_set (Int (f1, f2)) = mk_inf (mk_set f1, mk_set f2)
     val pat = foldr1 (mk_prod1 Ts) (map (term_of_pattern Ts) pats)