src/Pure/Thy/thy_parse.ML
changeset 3780 ac23a9ab3cd6
parent 3770 294b5905f4eb
child 3797 05e47c7cc6fd
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Mon Oct 06 18:27:55 1997 +0200
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Mon Oct 06 18:29:11 1997 +0200
     1.3 @@ -477,6 +477,7 @@
     1.4          \\n"
     1.5          ^ extxt ^ "\n\
     1.6          \\n\
     1.7 +        \|> Theory.add_path \"/\"\n\
     1.8          \|> Theory.add_name " ^ quote thy_name ^ ";\n\
     1.9          \\n\
    1.10          \val _ = store_theory (thy, " ^ quote thy_name ^ ");\n\
    1.11 @@ -545,6 +546,7 @@
    1.12    axm_section "defs" "|> Theory.add_defs" axiom_decls,
    1.13    axm_section "constdefs" "|> Theory.add_consts" constaxiom_decls,
    1.14    axm_section "axclass" "|> AxClass.add_axclass" axclass_decl,
    1.15 -  section "instance" "" instance_decl];
    1.16 +  section "instance" "" instance_decl,
    1.17 +  section "path" "|> Theory.add_path" name];
    1.18  
    1.19  end;