# HG changeset patch
# User traytel
# Date 1393621213 -3600
# Node ID 63d63d854fae399d27ec9df41bdf6f4b7d4ae13b
# Parent  d27e7872dd107d684f520050b03b487f90036309
made SML/NJ happier

diff -r d27e7872dd10 -r 63d63d854fae src/HOL/Tools/BNF/bnf_fp_n2m.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Fri Feb 28 18:11:11 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Fri Feb 28 22:00:13 2014 +0100
@@ -436,7 +436,7 @@
           @{thms fst_convol map_pair_o_convol convol_o}
           @{thms case_sum_o_inj(1) case_sum_o_sum_map o_case_sum};
 
-        val eq_thm_prop_untyped = op Term.aconv_untyped o pairself Thm.full_prop_of;
+        val eq_thm_prop_untyped = Term.aconv_untyped o pairself Thm.full_prop_of;
 
         val map_thms = no_refl (maps (fn bnf =>
            let val map_comp0 = map_comp0_of_bnf bnf RS sym