src/HOL/Tools/hologic.ML
changeset 32264 0be31453f698
parent 31736 926ebca5a145
child 32287 65d5c5b30747
     1.1 --- a/src/HOL/Tools/hologic.ML	Tue Jul 28 13:37:08 2009 +0200
     1.2 +++ b/src/HOL/Tools/hologic.ML	Tue Jul 28 13:37:09 2009 +0200
     1.3 @@ -153,13 +153,13 @@
     1.4  fun mk_set T ts =
     1.5    let
     1.6      val sT = mk_setT T;
     1.7 -    val empty = Const ("Set.empty", sT);
     1.8 +    val empty = Const ("Orderings.bot_class.bot", sT);
     1.9      fun insert t u = Const ("Set.insert", T --> sT --> sT) $ t $ u;
    1.10    in fold_rev insert ts empty end;
    1.11  
    1.12 -fun mk_UNIV T = Const ("Set.UNIV", mk_setT T);
    1.13 +fun mk_UNIV T = Const ("Orderings.top_class.top", mk_setT T);
    1.14  
    1.15 -fun dest_set (Const ("Set.empty", _)) = []
    1.16 +fun dest_set (Const ("Orderings.bot_class.bot", _)) = []
    1.17    | dest_set (Const ("Set.insert", _) $ t $ u) = t :: dest_set u
    1.18    | dest_set t = raise TERM ("dest_set", [t]);
    1.19