src/HOL/Tools/hologic.ML
changeset 31456 55edadbd43d5
parent 31205 98370b26c2ce
child 31463 c5681ed50eab
     1.1 --- a/src/HOL/Tools/hologic.ML	Thu Jun 04 15:28:59 2009 +0200
     1.2 +++ b/src/HOL/Tools/hologic.ML	Thu Jun 04 15:28:59 2009 +0200
     1.3 @@ -152,13 +152,13 @@
     1.4    let
     1.5      val sT = mk_setT T;
     1.6      val empty = Const ("Set.empty", sT);
     1.7 -    fun insert t u = Const ("insert", T --> sT --> sT) $ t $ u;
     1.8 +    fun insert t u = Const ("Set.insert", T --> sT --> sT) $ t $ u;
     1.9    in fold_rev insert ts empty end;
    1.10  
    1.11  fun mk_UNIV T = Const ("Set.UNIV", mk_setT T);
    1.12  
    1.13 -fun dest_set (Const ("Orderings.bot", _)) = []
    1.14 -  | dest_set (Const ("insert", _) $ t $ u) = t :: dest_set u
    1.15 +fun dest_set (Const ("Set.empty", _)) = []
    1.16 +  | dest_set (Const ("Set.insert", _) $ t $ u) = t :: dest_set u
    1.17    | dest_set t = raise TERM ("dest_set", [t]);
    1.18  
    1.19  fun Collect_const T = Const ("Collect", (T --> boolT) --> mk_setT T);