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.
passing names and types of all bounds around in the simproc
authorbulwahn
Sat, 20 Oct 2012 09:09:32 +0200
changeset 49943 6a26fed71755
parent 49942 50e457bbc5fe
child 49944 28cd3c9ca278
passing names and types of all bounds around in the simproc
src/HOL/Tools/set_comprehension_pointfree.ML file | annotate | diff | comparison | revisions 
--- 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)
isabelle