src/Pure/Thy/export_theory.ML
changeset 68830 44ec6fdaacf8
parent 68727 ec0b2833cfc4
child 68862 47e9912c53c3
     1.1 --- a/src/Pure/Thy/export_theory.ML	Tue Aug 28 11:40:11 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Tue Aug 28 12:07:30 2018 +0200
     1.3 @@ -66,8 +66,9 @@
     1.4        let
     1.5          val {serial, pos, ...} = Name_Space.the_entry space name;
     1.6          val props =
     1.7 -          Markup.serial_properties serial @
     1.8 -          Position.offset_properties_of (adjust_pos pos);
     1.9 +          Position.offset_properties_of (adjust_pos pos) @
    1.10 +          Position.id_properties_of pos @
    1.11 +          Markup.serial_properties serial;
    1.12        in (Markup.entityN, (Markup.nameN, name) :: props) end;
    1.13  
    1.14      fun export_entities export_name export get_space decls =