--- 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