src/Pure/Thy/thy_parse.ML
changeset 4020 f88775cc8d17
parent 4011 c161162bc8c5
child 4047 67b5552b1067
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Tue Oct 28 17:31:55 1997 +0100
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Tue Oct 28 17:32:38 1997 +0100
     1.3 @@ -375,7 +375,7 @@
     1.4      val (axms_defs, axms_names) =
     1.5        mk_axiom_decls (map (fn ((id, _), def) => (id ^ "_def", def)) x);
     1.6    in ((mk_big_list o map mk_triple2 o map (apfst quote o fst)) x ^
     1.7 -       "\n\n|> Theory.add_defs\n" ^ axms_defs, axms_names)
     1.8 +       "\n\n|> PureThy.add_store_defs\n" ^ axms_defs, axms_names)
     1.9    end;
    1.10  
    1.11  val constaxiom_decls =
    1.12 @@ -554,8 +554,8 @@
    1.13    section "consts" "|> Theory.add_consts" const_decls,
    1.14    section "syntax" "|> Theory.add_modesyntax" syntax_decls,
    1.15    section "translations" "|> Theory.add_trrules" trans_decls,
    1.16 -  axm_section "rules" "|> Theory.add_axioms" axiom_decls,
    1.17 -  axm_section "defs" "|> Theory.add_defs" axiom_decls,
    1.18 +  axm_section "rules" "|> PureThy.add_store_axioms" axiom_decls,
    1.19 +  axm_section "defs" "|> PureThy.add_store_defs" axiom_decls,
    1.20    section "oracle" "|> Theory.add_oracle" oracle_decl,
    1.21    axm_section "constdefs" "|> Theory.add_consts" constaxiom_decls,
    1.22    axm_section "axclass" "|> AxClass.add_axclass" axclass_decl,