1.1 --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Tue Sep 18 03:33:53 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Tue Sep 18 09:15:53 2012 +0200
     1.3 @@ -1701,9 +1701,10 @@
     1.4          fun wit_tac _ = mk_wit_tac n (flat set_simp_thmss) (maps wit_thms_of_bnf bnfs);
     1.5  
     1.6          val (Ibnfs, lthy) =
     1.7 -          fold_map6 (fn tacs => fn b => fn map => fn sets => fn T => fn wits =>
     1.8 +          fold_map6 (fn tacs => fn b => fn map => fn sets => fn T => fn wits => fn lthy =>
     1.9              bnf_def Dont_Inline user_policy I tacs wit_tac (SOME deads)
    1.10 -              ((((b, fold_rev Term.absfree fs' map), sets), absdummy T bd), wits))
    1.11 +              ((((b, fold_rev Term.absfree fs' map), sets), absdummy T bd), wits) lthy
    1.12 +            |> register_bnf (Local_Theory.full_name lthy b))
    1.13            tacss bs fs_maps setss_by_bnf Ts fld_witss lthy;
    1.14  
    1.15          val fold_maps = Local_Defs.fold lthy (map (fn bnf =>