src/HOL/Tools/BNF/bnf_fp_n2m.ML
changeset 55810 63d63d854fae
parent 55803 74d3fe9031d8
child 55819 e21d83c8e1c7
     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