src/HOL/Tools/TFL/usyntax.ML

   in list_comb(c,[mk_abs r])
   end;
 
 
 fun mk_conj{conj1,conj2} =
-   let val c = Const(@{const_name "op &"},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
+   let val c = Const(@{const_name HOL.conj},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
    in list_comb(c,[conj1,conj2])
    end;
 
 fun mk_disj{disj1,disj2} =
-   let val c = Const(@{const_name "op |"},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
+   let val c = Const(@{const_name HOL.disj},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
    in list_comb(c,[disj1,disj2])
    end;
 
 fun prod_ty ty1 ty2 = HOLogic.mk_prodT (ty1,ty2);
 

   | dest_exists _ = raise USYN_ERR "dest_exists" "not an existential";
 
 fun dest_neg(Const(@{const_name Not},_) $ M) = M
   | dest_neg _ = raise USYN_ERR "dest_neg" "not a negation";
 
-fun dest_conj(Const(@{const_name "op &"},_) $ M $ N) = {conj1=M, conj2=N}
+fun dest_conj(Const(@{const_name HOL.conj},_) $ M $ N) = {conj1=M, conj2=N}
   | dest_conj _ = raise USYN_ERR "dest_conj" "not a conjunction";
 
-fun dest_disj(Const(@{const_name "op |"},_) $ M $ N) = {disj1=M, disj2=N}
+fun dest_disj(Const(@{const_name HOL.disj},_) $ M $ N) = {disj1=M, disj2=N}
   | dest_disj _ = raise USYN_ERR "dest_disj" "not a disjunction";
 
 fun mk_pair{fst,snd} =
    let val ty1 = type_of fst
        val ty2 = type_of snd