src/HOL/Codatatype/Tools/bnf_wrap.ML
changeset 49111 9d511132394e
parent 49075 ed769978dc8d
child 49113 ef3eea7ae251
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 04 12:12:03 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 04 13:02:25 2012 +0200
     1.3 @@ -7,6 +7,8 @@
     1.4  
     1.5  signature BNF_WRAP =
     1.6  sig
     1.7 +  val wrap: ({prems: thm list, context: Proof.context} -> tactic) list list ->
     1.8 +    (term list * term) * (binding list * binding list list) -> Proof.context -> local_theory
     1.9  end;
    1.10  
    1.11  structure BNF_Wrap : BNF_WRAP =
    1.12 @@ -405,6 +407,11 @@
    1.13      (goals, after_qed, lthy')
    1.14    end;
    1.15  
    1.16 +fun wrap tacss = (fn (goalss, after_qed, lthy) =>
    1.17 +  map2 (map2 (Skip_Proof.prove lthy [] [])) goalss tacss
    1.18 +  |> (fn thms => after_qed thms lthy)) oo
    1.19 +  prepare_wrap (singleton o Type_Infer_Context.infer_types)
    1.20 +
    1.21  val parse_bindings = Parse.$$$ "[" |--  Parse.list Parse.binding --| Parse.$$$ "]";
    1.22  
    1.23  val parse_bindingss = Parse.$$$ "[" |-- Parse.list parse_bindings --| Parse.$$$ "]";