--- a/src/HOL/Tools/BNF/bnf_util.ML Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_util.ML Thu Mar 06 15:40:33 2014 +0100
@@ -94,7 +94,7 @@
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
@@ -438,11 +438,11 @@
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"*)