explode #> scan_valids #> implode

     explode #> scan_valids #> implode

   end;

   end;

 val type_name = sanitize_name o Long_Name.base_name;

 val type_name = sanitize_name o Long_Name.base_name;

     (AxClass.declare_overloaded (c, U) ##>> AxClass.define_overloaded b_def (c, rhs))

     (AxClass.declare_overloaded (c, U) ##>> AxClass.define_overloaded b_def (c, rhs))

   ##> (map_instantiation o apsnd) (filter_out (fn (_, (v', _)) => v' = v))

   ##> (map_instantiation o apsnd) (filter_out (fn (_, (v', _)) => v' = v))

   ##> Local_Theory.target synchronize_inst_syntax;

   ##> Local_Theory.target synchronize_inst_syntax;

 fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =

 fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =

 fun gen_instantiation_instance do_proof after_qed lthy =

 fun gen_instantiation_instance do_proof after_qed lthy =

   let

   let

     val (tycos, vs, sort) = (#arities o the_instantiation) lthy;

     val (tycos, vs, sort) = (#arities o the_instantiation) lthy;

     val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, map snd vs, sort)) tycos;

     val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, map snd vs, sort)) tycos;

     fun after_qed' results =

     fun after_qed' results =

       #> after_qed;

       #> after_qed;

   in

   in

     lthy

     lthy

     |> do_proof after_qed' arities_proof

     |> do_proof after_qed' arities_proof

   end;

   end;