src/Pure/Thy/thy_parse.ML
changeset 3780 ac23a9ab3cd6
parent 3770 294b5905f4eb
child 3797 05e47c7cc6fd
equal deleted inserted replaced
3779:ce8594f7e0c6 3780:ac23a9ab3cd6
   475         \|> Theory.add_trfunsT typed_print_translation \n\
   475         \|> Theory.add_trfunsT typed_print_translation \n\
   476         \|> Theory.add_tokentrfuns token_translation \n\
   476         \|> Theory.add_tokentrfuns token_translation \n\
   477         \\n"
   477         \\n"
   478         ^ extxt ^ "\n\
   478         ^ extxt ^ "\n\
   479         \\n\
   479         \\n\
       
   480         \|> Theory.add_path \"/\"\n\
   480         \|> Theory.add_name " ^ quote thy_name ^ ";\n\
   481         \|> Theory.add_name " ^ quote thy_name ^ ";\n\
   481         \\n\
   482         \\n\
   482         \val _ = store_theory (thy, " ^ quote thy_name ^ ");\n\
   483         \val _ = store_theory (thy, " ^ quote thy_name ^ ");\n\
   483         \\n\
   484         \\n\
   484         \\n"
   485         \\n"
   543   section "translations" "|> Theory.add_trrules" trans_decls,
   544   section "translations" "|> Theory.add_trrules" trans_decls,
   544   axm_section "rules" "|> Theory.add_axioms" axiom_decls,
   545   axm_section "rules" "|> Theory.add_axioms" axiom_decls,
   545   axm_section "defs" "|> Theory.add_defs" axiom_decls,
   546   axm_section "defs" "|> Theory.add_defs" axiom_decls,
   546   axm_section "constdefs" "|> Theory.add_consts" constaxiom_decls,
   547   axm_section "constdefs" "|> Theory.add_consts" constaxiom_decls,
   547   axm_section "axclass" "|> AxClass.add_axclass" axclass_decl,
   548   axm_section "axclass" "|> AxClass.add_axclass" axclass_decl,
   548   section "instance" "" instance_decl];
   549   section "instance" "" instance_decl,
       
   550   section "path" "|> Theory.add_path" name];
   549 
   551 
   550 end;
   552 end;