export "wrap" function

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

--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 04 12:12:03 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 04 13:02:25 2012 +0200
@@ -7,6 +7,8 @@
 
 signature BNF_WRAP =
 sig
+  val wrap: ({prems: thm list, context: Proof.context} -> tactic) list list ->
+    (term list * term) * (binding list * binding list list) -> Proof.context -> local_theory
 end;
 
 structure BNF_Wrap : BNF_WRAP =
@@ -405,6 +407,11 @@
     (goals, after_qed, lthy')
   end;
 
+fun wrap tacss = (fn (goalss, after_qed, lthy) =>
+  map2 (map2 (Skip_Proof.prove lthy [] [])) goalss tacss
+  |> (fn thms => after_qed thms lthy)) oo
+  prepare_wrap (singleton o Type_Infer_Context.infer_types)
+
 val parse_bindings = Parse.$$$ "[" |--  Parse.list Parse.binding --| Parse.$$$ "]";
 
 val parse_bindingss = Parse.$$$ "[" |-- Parse.list parse_bindings --| Parse.$$$ "]";