src/HOL/Codatatype/Tools/bnf_gfp.ML
changeset 49018 b2884253b421
parent 48975 7f79f94a432c
child 49029 f0ecfa9575a9
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Thu Aug 30 09:47:46 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Thu Aug 30 09:47:46 2012 +0200
     1.3 @@ -2630,7 +2630,7 @@
     1.4  
     1.5          val (Jbnfs, lthy) =
     1.6            fold_map6 (fn tacs => fn b => fn map => fn sets => fn T => fn wits =>
     1.7 -            add_bnf Dont_Inline user_policy I tacs wit_tac (SOME deads)
     1.8 +            bnf_def Dont_Inline user_policy I tacs wit_tac (SOME deads)
     1.9                ((((b, fold_rev Term.absfree fs' map), sets), absdummy T bd), wits))
    1.10            tacss bs fs_maps setss_by_bnf Ts fld_witss lthy;
    1.11