src/HOL/Tools/BNF/bnf_util.ML

   val mk_converse: term -> term
   val mk_conversep: term -> term
   val mk_cprod: term -> term -> term
   val mk_csum: term -> term -> term
   val mk_dir_image: term -> term -> term
-  val mk_fun_rel: term -> term -> term
+  val mk_rel_fun: term -> term -> term
   val mk_image: term -> term
   val mk_in: term list -> term list -> typ -> term
   val mk_leq: term -> term -> term
   val mk_ordLeq: term -> term -> term
   val mk_rel_comp: term * term -> term

 
 fun mk_dir_image r f =
   let val (T, U) = dest_funT (fastype_of f);
   in Const (@{const_name dir_image}, mk_relT (T, T) --> (T --> U) --> mk_relT (U, U)) $ r $ f end;
 
-fun mk_fun_rel R S =
+fun mk_rel_fun R S =
   let
     val ((RA, RB), RT) = `dest_pred2T (fastype_of R);
     val ((SA, SB), ST) = `dest_pred2T (fastype_of S);
-  in Const (@{const_name fun_rel}, RT --> ST --> mk_pred2T (RA --> SA) (RB --> SB)) $ R $ S end;
+  in Const (@{const_name rel_fun}, RT --> ST --> mk_pred2T (RA --> SA) (RB --> SB)) $ R $ S end;
 
 (*FIXME: "x"?*)
 (*(nth sets i) must be of type "T --> 'ai set"*)
 fun mk_in As sets T =
   let