src/HOL/Tools/BNF/bnf_util.ML

--- a/src/HOL/Tools/BNF/bnf_util.ML	Tue Oct 14 16:17:34 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Tue Oct 14 16:17:36 2014 +0200
@@ -385,7 +385,7 @@
   | mk_ordLeq_csum n m thm = @{thm ordLeq_transitive} OF
     [mk_ordLeq_csum (n - 1) (m - 1) thm, @{thm ordLeq_csum2[OF Card_order_csum]}];
 
-fun mk_rel_funDN n = funpow n (fn thm => thm RS @{thm rel_funD});
+fun mk_rel_funDN n = funpow n (fn thm => thm RS rel_funD);
 
 val mk_rel_funDN_rotated = rotate_prems ~1 oo mk_rel_funDN;