src/HOL/BNF/Tools/bnf_util.ML

   val mk_ordLeq: term -> term -> term
   val mk_rel_comp: term * term -> term
   val mk_subset: term -> term -> term
   val mk_wpull: term -> term -> term -> term -> term -> (term * term) option -> term -> term -> term
 
+  val rapp: term -> term -> term
+
   val list_all_free: term list -> term -> term
   val list_exists_free: term list -> term -> term
 
   (*parameterized terms*)
   val mk_nthN: int -> term -> int -> term

   let val T = (case xs of [] => defT | (x::_) => fastype_of x);
   in Const (@{const_name collect}, HOLogic.mk_setT T --> T) $ (HOLogic.mk_set T xs) end;
 
 fun mk_permute src dest xs = map (nth xs o (fn x => find_index ((curry op =) x) src)) dest;
 
+fun rapp u t = betapply (t, u);
+
 val list_all_free =
   fold_rev (fn free => fn P =>
     let val (x, T) = Term.dest_Free free;
     in HOLogic.all_const T $ Term.absfree (x, T) P end);