1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Fri Feb 28 18:11:11 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Fri Feb 28 22:00:13 2014 +0100
     1.3 @@ -436,7 +436,7 @@
     1.4            @{thms fst_convol map_pair_o_convol convol_o}
     1.5            @{thms case_sum_o_inj(1) case_sum_o_sum_map o_case_sum};
     1.6  
     1.7 -        val eq_thm_prop_untyped = op Term.aconv_untyped o pairself Thm.full_prop_of;
     1.8 +        val eq_thm_prop_untyped = Term.aconv_untyped o pairself Thm.full_prop_of;
     1.9  
    1.10          val map_thms = no_refl (maps (fn bnf =>
    1.11             let val map_comp0 = map_comp0_of_bnf bnf RS sym