src/HOL/Tools/BNF/bnf_util.ML

--- a/src/HOL/Tools/BNF/bnf_util.ML	Mon Mar 30 18:33:22 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Mon Mar 30 20:59:14 2015 +0200
@@ -313,7 +313,7 @@
   end;
 
 fun mk_leq t1 t2 =
-  Const (@{const_name less_eq}, (fastype_of t1) --> (fastype_of t2) --> HOLogic.boolT) $ t1 $ t2;
+  Const (@{const_name less_eq}, fastype_of t1 --> fastype_of t2 --> HOLogic.boolT) $ t1 $ t2;
 
 fun mk_card_binop binop typop t1 t2 =
   let