--- a/src/HOL/Tools/hologic.ML Tue Jul 28 13:37:08 2009 +0200
+++ b/src/HOL/Tools/hologic.ML Tue Jul 28 13:37:09 2009 +0200
@@ -153,13 +153,13 @@
fun mk_set T ts =
let
val sT = mk_setT T;
- val empty = Const ("Set.empty", sT);
+ val empty = Const ("Orderings.bot_class.bot", sT);
fun insert t u = Const ("Set.insert", T --> sT --> sT) $ t $ u;
in fold_rev insert ts empty end;
-fun mk_UNIV T = Const ("Set.UNIV", mk_setT T);
+fun mk_UNIV T = Const ("Orderings.top_class.top", mk_setT T);
-fun dest_set (Const ("Set.empty", _)) = []
+fun dest_set (Const ("Orderings.bot_class.bot", _)) = []
| dest_set (Const ("Set.insert", _) $ t $ u) = t :: dest_set u
| dest_set t = raise TERM ("dest_set", [t]);