src/HOL/Tools/BNF/bnf_util.ML

--- a/src/HOL/Tools/BNF/bnf_util.ML	Tue Feb 18 23:08:58 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Tue Feb 18 23:08:59 2014 +0100
@@ -419,7 +419,7 @@
     val AT = fst (dest_relT T);
   in
     Const (@{const_name card_order_on}, HOLogic.mk_setT AT --> T --> HOLogic.boolT) $
-      (HOLogic.mk_UNIV AT) $ bd
+      HOLogic.mk_UNIV AT $ bd
   end;
 
 fun mk_Card_order bd =