# HG changeset patch
# User haftmann
# Date 1324738498 -3600
# Node ID e3accf78bb07ce074d4e7bcf53ba6104bca9bb14
# Parent  9dc0d950baa9fd1464cd5c1147dc687813f0c36a
`set` is now a proper type constructor

diff -r 9dc0d950baa9 -r e3accf78bb07 src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Sat Dec 24 15:53:12 2011 +0100
+++ b/src/HOL/Tools/hologic.ML	Sat Dec 24 15:54:58 2011 +0100
@@ -162,9 +162,9 @@
 
 fun mk_induct_forall T = Const ("HOL.induct_forall", (T --> boolT) --> boolT);
 
-fun mk_setT T = T --> boolT;
+fun mk_setT T = Type ("Set.set", [T]);
 
-fun dest_setT (Type ("fun", [T, Type ("HOL.bool", [])])) = T
+fun dest_setT (Type ("Set.set", [T])) = T
   | dest_setT T = raise TYPE ("dest_setT: set type expected", [T], []);
 
 fun mk_set T ts =