# HG changeset patch
# User wenzelm
# Date 893842019 -7200
# Node ID 58b5006d36cc29564fe3bfb0ee8c788c9f4d68c5
# Parent  cbbc53963aaa28de5f4f8e2ee086e5ec946f00e4
replaced thy_setup by 'setup' section;
adapted to new PureThy.add_axioms / PureThy.add_defs;
added 'nonterminals' section;

diff -r cbbc53963aaa -r 58b5006d36cc src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Wed Apr 29 11:25:26 1998 +0200
+++ b/src/Pure/Thy/thy_parse.ML	Wed Apr 29 11:26:59 1998 +0200
@@ -344,8 +344,7 @@
   \ val print_translation = [];\n\
   \ val typed_print_translation = [];\n\
   \ val print_ast_translation = [];\n\
-  \ val token_translation = [];\n\
-  \ val thy_setup = []";
+  \ val token_translation = [];";
 
 val trfun_args =
   "(parse_ast_translation, parse_translation, \
@@ -373,7 +372,7 @@
     val (axms_defs, axms_names) =
       mk_axiom_decls (map (fn ((id, _), def) => (id ^ "_def", def)) x);
   in ((mk_big_list o map mk_triple2 o map (apfst quote o fst)) x ^
-       "\n\n|> PureThy.add_store_defs\n" ^ axms_defs, axms_names)
+       "\n\n|> (PureThy.add_defs o map Attribute.none)\n" ^ axms_defs, axms_names)
   end;
 
 val constaxiom_decls =
@@ -419,7 +418,7 @@
 fun empty_decl toks = (empty >> K "") toks;
 
 val global_path =
-  "|> (fn thy => if ! global_names then thy else Theory.add_path \"/\" thy)";
+  "|> (fn thy => if ! global_names then thy else Theory.root_path thy)";
 
 val local_path =
   global_path ^ "\n\
@@ -503,7 +502,6 @@
     \\n"
     ^ local_path ^
     "\n\
-    \|> Theory.setup thy_setup\n\
     \|> Theory.add_trfuns\n"
     ^ trfun_args ^ "\n\
     \|> Theory.add_trfunsT typed_print_translation\n\
@@ -556,12 +554,13 @@
  [section "classes" "|> Theory.add_classes" class_decls,
   section "default" "|> Theory.add_defsort" sort,
   section "types" "" type_decls,
+  section "nonterminals" "|> Theory.add_nonterminals" (repeat1 name >> mk_list),
   section "arities" "|> Theory.add_arities" arity_decls,
   section "consts" "|> Theory.add_consts" const_decls,
   section "syntax" "|> Theory.add_modesyntax" syntax_decls,
   section "translations" "|> Theory.add_trrules" trans_decls,
-  axm_section "rules" "|> PureThy.add_store_axioms" axiom_decls,
-  axm_section "defs" "|> PureThy.add_store_defs" axiom_decls,
+  axm_section "rules" "|> (PureThy.add_axioms o map Attribute.none)" axiom_decls,
+  axm_section "defs" "|> (PureThy.add_defs o map Attribute.none)" axiom_decls,
   section "oracle" "|> Theory.add_oracle" oracle_decl,
   axm_section "constdefs" "|> Theory.add_consts" constaxiom_decls,
   axm_section "axclass" "|> AxClass.add_axclass" axclass_decl,
@@ -569,6 +568,7 @@
   section "path" "|> Theory.add_path" name,
   section "global" global_path empty_decl,
   section "local" local_path empty_decl,
+  section "setup" "|> Theory.apply" long_id,
   section "MLtext" "" verbatim];