src/Pure/Thy/export_theory.ML
changeset 68231 0004e7a9fa10
parent 68230 9bee37c2ac2b
child 68232 4b93573ac5b4
equal deleted inserted replaced
68230:9bee37c2ac2b 68231:0004e7a9fa10
    30     (* parents *)
    30     (* parents *)
    31 
    31 
    32     val parents = Theory.parents_of thy;
    32     val parents = Theory.parents_of thy;
    33     val _ =
    33     val _ =
    34       export_body thy "parents"
    34       export_body thy "parents"
    35         let open XML.Encode
    35         (XML.Encode.string (cat_lines (map Context.theory_long_name parents)));
    36         in list string (map Context.theory_long_name parents) end;
       
    37 
    36 
    38 
    37 
    39     (* entities *)
    38     (* entities *)
    40 
    39 
    41     fun entity_markup space name =
    40     fun entity_markup space name =