# HG changeset patch
# User bulwahn
# Date 1350716972 -7200
# Node ID 6a26fed717550ee16a78ee7116d6845f93fba518
# Parent  50e457bbc5fe40de8f43f4daa578b99302795902
passing names and types of all bounds around in the simproc

diff -r 50e457bbc5fe -r 6a26fed71755 src/HOL/Tools/set_comprehension_pointfree.ML
--- a/src/HOL/Tools/set_comprehension_pointfree.ML	Thu Oct 18 10:06:27 2012 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Sat Oct 20 09:09:32 2012 +0200
@@ -206,7 +206,7 @@
     val unused_bounds = subtract (op =) (distinct (op =) (maps loose_bnos conjs'))
       (0 upto (length vs - 1))
     val (pats, fm) =
-      mk_formula vs (foldr1 HOLogic.mk_conj (conjs' @ map mk_mem_UNIV unused_bounds))
+      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)
       | 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)