# HG changeset patch
# User bulwahn
# Date 1320045776 -3600
# Node ID 6fd16567710954c6f9c3363bc7de9f650ec6a22d
# Parent  ca9e66c523a25b1b0e24552f7e4e10a22cffdcdc
tuned

diff -r ca9e66c523a2 -r 6fd165677109 src/HOL/Tools/Quotient/quotient_typ.ML
--- a/src/HOL/Tools/Quotient/quotient_typ.ML	Sun Oct 30 22:35:18 2011 +0100
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Mon Oct 31 08:22:56 2011 +0100
@@ -32,14 +32,10 @@
       [("x", rty), ("c", HOLogic.mk_setT rty)]
       |> Variable.variant_frees lthy [rel]
       |> map Free
-    fun mk_collect T =
-      Const (@{const_name Collect}, (T --> @{typ bool}) --> HOLogic.mk_setT T)
-    val collect_in = mk_collect rty
-    val collect_out = mk_collect (HOLogic.mk_setT rty)
   in
-    collect_out $ (lambda c (HOLogic.exists_const rty $
+    HOLogic.Collect_const (HOLogic.mk_setT rty) $ (lambda c (HOLogic.exists_const rty $
         lambda x (HOLogic.mk_conj (rel $ x $ x,
-        HOLogic.mk_eq (c, collect_in $ (rel $ x))))))
+        HOLogic.mk_eq (c, HOLogic.Collect_const rty $ (rel $ x))))))
   end