# HG changeset patch
# User berghofe
# Date 1210150615 -7200
# Node ID e2b1e6868c2f2a5054462a1cb6d72cb304c1273a
# Parent  0af0f674845d2492af9a033b0bc689976605e956
Adapted functions mk_setT and dest_setT to encoding of sets as predicates.

diff -r 0af0f674845d -r e2b1e6868c2f src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Wed May 07 10:56:52 2008 +0200
+++ b/src/HOL/hologic.ML	Wed May 07 10:56:55 2008 +0200
@@ -135,9 +135,9 @@
 val true_const =  Const ("True", boolT);
 val false_const = Const ("False", boolT);
 
-fun mk_setT T = Type ("set", [T]);
+fun mk_setT T = T --> boolT;
 
-fun dest_setT (Type ("set", [T])) = T
+fun dest_setT (Type ("fun", [T, Type ("bool", [])])) = T
   | dest_setT T = raise TYPE ("dest_setT: set type expected", [T], []);