| changeset 45977 | e3accf78bb07 |
| parent 45740 | 132a3e1c0fe5 |
| child 46216 | 7fcdb5562461 |
--- 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 =