src/HOL/Tools/hologic.ML
changeset 38795 848be46708dc
parent 38786 e46e7a9cb622
child 38857 97775f3e8722
     1.1 --- a/src/HOL/Tools/hologic.ML	Fri Aug 27 10:55:20 2010 +0200
     1.2 +++ b/src/HOL/Tools/hologic.ML	Fri Aug 27 10:56:46 2010 +0200
     1.3 @@ -208,8 +208,8 @@
     1.4    let val (th1, th2) = conj_elim th
     1.5    in conj_elims th1 @ conj_elims th2 end handle THM _ => [th];
     1.6  
     1.7 -val conj = @{term "op &"}
     1.8 -and disj = @{term "op |"}
     1.9 +val conj = @{term HOL.conj}
    1.10 +and disj = @{term HOL.disj}
    1.11  and imp = @{term implies}
    1.12  and Not = @{term Not};
    1.13  
    1.14 @@ -218,14 +218,14 @@
    1.15  and mk_imp (t1, t2) = imp $ t1 $ t2
    1.16  and mk_not t = Not $ t;
    1.17  
    1.18 -fun dest_conj (Const ("op &", _) $ t $ t') = t :: dest_conj t'
    1.19 +fun dest_conj (Const ("HOL.conj", _) $ t $ t') = t :: dest_conj t'
    1.20    | dest_conj t = [t];
    1.21  
    1.22 -fun dest_disj (Const ("op |", _) $ t $ t') = t :: dest_disj t'
    1.23 +fun dest_disj (Const ("HOL.disj", _) $ t $ t') = t :: dest_disj t'
    1.24    | dest_disj t = [t];
    1.25  
    1.26  (*Like dest_disj, but flattens disjunctions however nested*)
    1.27 -fun disjuncts_aux (Const ("op |", _) $ t $ t') disjs = disjuncts_aux t (disjuncts_aux t' disjs)
    1.28 +fun disjuncts_aux (Const ("HOL.disj", _) $ t $ t') disjs = disjuncts_aux t (disjuncts_aux t' disjs)
    1.29    | disjuncts_aux t disjs = t::disjs;
    1.30  
    1.31  fun disjuncts t = disjuncts_aux t [];