`set` is now a proper type constructor

--- 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 =