src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
changeset 57932 c29659f77f8d
parent 57898 f7f75b33d6c8
child 57983 6edc3529bb4e
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Aug 13 22:29:43 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Aug 14 13:20:54 2014 +0200
     1.3 @@ -471,7 +471,7 @@
     1.4    #>> map (fn thm => Thm.permute_prems 0 (~1) (thm RS prop))
     1.5    ##> (fn thm => Thm.permute_prems 0 (~nn)
     1.6      (if nn = 1 then thm RS prop
     1.7 -     else funpow nn (fn thm => Local_Defs.unfold lthy @{thms conj_assoc} (thm RS prop_conj)) thm));
     1.8 +     else funpow nn (fn thm => unfold_thms lthy @{thms conj_assoc} (thm RS prop_conj)) thm));
     1.9  
    1.10  fun mk_induct_attrs ctrss =
    1.11    let