1.1 --- a/src/HOL/Codatatype/Tools/bnf_def.ML	Tue Sep 04 12:12:03 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_def.ML	Tue Sep 04 13:02:25 2012 +0200
     1.3 @@ -1180,11 +1180,11 @@
     1.4        |> map2 (Conjunction.elim_balanced o length) wit_goalss
     1.5        |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0))
     1.6    in
     1.7 -    (map2 (Thm.close_derivation oo Skip_Proof.prove lthy [] [])
     1.8 -      goals (map (unfold_defs_tac lthy defs) tacs))
     1.9 +    map2 (Thm.close_derivation oo Skip_Proof.prove lthy [] [])
    1.10 +      goals (map (unfold_defs_tac lthy defs) tacs)
    1.11      |> (fn thms => after_qed (map single thms @ wit_thms) lthy)
    1.12    end) oo prepare_def const_policy fact_policy qualify
    1.13 -  (fn ctxt => singleton (Type_Infer_Context.infer_types ctxt)) Ds;
    1.14 +  (singleton o Type_Infer_Context.infer_types) Ds;
    1.15  
    1.16  val bnf_def_cmd = (fn (goals, wit_goals, after_qed, lthy, defs) =>
    1.17    Proof.unfolding ([[(defs, [])]])

     2.1 --- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 04 12:12:03 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 04 13:02:25 2012 +0200
     2.3 @@ -7,6 +7,8 @@
     2.4  
     2.5  signature BNF_WRAP =
     2.6  sig
     2.7 +  val wrap: ({prems: thm list, context: Proof.context} -> tactic) list list ->
     2.8 +    (term list * term) * (binding list * binding list list) -> Proof.context -> local_theory
     2.9  end;
    2.10  
    2.11  structure BNF_Wrap : BNF_WRAP =
    2.12 @@ -405,6 +407,11 @@
    2.13      (goals, after_qed, lthy')
    2.14    end;
    2.15  
    2.16 +fun wrap tacss = (fn (goalss, after_qed, lthy) =>
    2.17 +  map2 (map2 (Skip_Proof.prove lthy [] [])) goalss tacss
    2.18 +  |> (fn thms => after_qed thms lthy)) oo
    2.19 +  prepare_wrap (singleton o Type_Infer_Context.infer_types)
    2.20 +
    2.21  val parse_bindings = Parse.$$$ "[" |--  Parse.list Parse.binding --| Parse.$$$ "]";
    2.22  
    2.23  val parse_bindingss = Parse.$$$ "[" |-- Parse.list parse_bindings --| Parse.$$$ "]";