val _ = ThyOutput.antiquotation "code_stmts"

 val _ = ThyOutput.antiquotation "code_stmts"

   (parse_const_terms -- Scan.repeat parse_names -- Scan.lift (Args.parens Args.name))

   (parse_const_terms -- Scan.repeat parse_names -- Scan.lift (Args.parens Args.name))

   (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), target) =>

   (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), target) =>

     let val thy = ProofContext.theory_of ctxt in

     let val thy = ProofContext.theory_of ctxt in

       Code_Target.code_of thy

       Code_Target.code_of thy

         (fn naming => maps (fn f => f thy naming) mk_stmtss)

         (fn naming => maps (fn f => f thy naming) mk_stmtss)

       |> typewriter

       |> typewriter

     end);

     end);

 end;

 end;