- let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
- SequentPp.XmlPp.print_sequent metasenv sequent in
- let sequent_doc =
- Xml2Gdome.document_of_xml Misc.domImpl sequent_gdome in
- let sequent_mml =
- ApplyStylesheets.apply_sequent_stylesheets sequent_doc
+ let sequent_mml,(ids_to_terms,ids_to_father_ids,ids_to_hypotheses) =
+ ApplyStylesheets.mml_of_cic_sequent metasenv sequent