1.1 --- a/src/HOL/Tools/hologic.ML	Thu Aug 26 13:44:50 2010 +0200
     1.2 +++ b/src/HOL/Tools/hologic.ML	Thu Aug 26 20:51:17 2010 +0200
     1.3 @@ -210,8 +210,8 @@
     1.4  
     1.5  val conj = @{term "op &"}
     1.6  and disj = @{term "op |"}
     1.7 -and imp = @{term "op -->"}
     1.8 -and Not = @{term "Not"};
     1.9 +and imp = @{term implies}
    1.10 +and Not = @{term Not};
    1.11  
    1.12  fun mk_conj (t1, t2) = conj $ t1 $ t2
    1.13  and mk_disj (t1, t2) = disj $ t1 $ t2
    1.14 @@ -230,7 +230,7 @@
    1.15  
    1.16  fun disjuncts t = disjuncts_aux t [];
    1.17  
    1.18 -fun dest_imp (Const ("op -->", _) $ A $ B) = (A, B)
    1.19 +fun dest_imp (Const ("HOL.implies", _) $ A $ B) = (A, B)
    1.20    | dest_imp  t = raise TERM ("dest_imp", [t]);
    1.21  
    1.22  fun dest_not (Const ("HOL.Not", _) $ t) = t