# HG changeset patch
# User boehmes
# Date 1319525316 -7200
# Node ID 93ac73160d7826ce9a505f01914c8865635a56c0
# Parent  b0cea4362430da9aaceb3397a3bfe6c7545d52cd
clarify types of terms: use proper set type

diff -r b0cea4362430 -r 93ac73160d78 src/HOL/Tools/SMT/z3_proof_methods.ML
--- a/src/HOL/Tools/SMT/z3_proof_methods.ML	Mon Oct 24 16:47:24 2011 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_methods.ML	Tue Oct 25 08:48:36 2011 +0200
@@ -25,11 +25,11 @@
 local
 
 val B = @{typ bool}
-fun mk_univ T = Const (@{const_name top}, T --> B)
+fun mk_univ T = Const (@{const_name top}, HOLogic.mk_setT T)
 fun mk_inj_on T U =
-  Const (@{const_name inj_on}, (T --> U) --> (T --> B) --> B)
+  Const (@{const_name inj_on}, (T --> U) --> HOLogic.mk_setT T --> B)
 fun mk_inv_into T U =
-  Const (@{const_name inv_into}, [T --> B, T --> U, U] ---> T)
+  Const (@{const_name inv_into}, [HOLogic.mk_setT T, T --> U, U] ---> T)
 
 fun mk_inv_of ctxt ct =
   let