src/Pure/Thy/thy_parse.ML
changeset 3764 fe7719aee219
parent 3528 f4b28e25ba99
child 3770 294b5905f4eb
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Wed Oct 01 17:36:51 1997 +0200
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Wed Oct 01 17:40:09 1997 +0200
     1.3 @@ -279,8 +279,8 @@
     1.4        [(parens (commas [t, mk_list xs, rhs, syn]), true)];
     1.5  
     1.6  fun mk_type_decls tys =
     1.7 -  "|> add_types\n" ^ mk_big_list (keyfilter tys false) ^ "\n\n\
     1.8 -  \|> add_tyabbrs\n" ^ mk_big_list (keyfilter tys true);
     1.9 +  "|> Theory.add_types\n" ^ mk_big_list (keyfilter tys false) ^ "\n\n\
    1.10 +  \|> Theory.add_tyabbrs\n" ^ mk_big_list (keyfilter tys true);
    1.11  
    1.12  
    1.13  val old_type_decl = names1 -- nat -- opt_infix >> mk_old_type_decl;
    1.14 @@ -362,7 +362,7 @@
    1.15      val (axms_defs, axms_names) =
    1.16        mk_axiom_decls (map (fn ((id, _), def) => (id ^ "_def", def)) x);
    1.17    in ((mk_big_list o map mk_triple2 o map (apfst quote o fst)) x ^
    1.18 -       "\n\n|> add_defs\n" ^ axms_defs, axms_names)
    1.19 +       "\n\n|> Theory.add_defs\n" ^ axms_defs, axms_names)
    1.20    end;
    1.21  
    1.22  val constaxiom_decls =
    1.23 @@ -470,14 +470,14 @@
    1.24          \\n\
    1.25          \val thy = thy\n\
    1.26          \\n\
    1.27 -        \|> add_trfuns\n"
    1.28 +        \|> Theory.add_trfuns\n"
    1.29          ^ trfun_args ^ "\n\
    1.30 -        \|> add_trfunsT typed_print_translation \n\
    1.31 -        \|> add_tokentrfuns token_translation \n\
    1.32 +        \|> Theory.add_trfunsT typed_print_translation \n\
    1.33 +        \|> Theory.add_tokentrfuns token_translation \n\
    1.34          \\n"
    1.35          ^ extxt ^ "\n\
    1.36          \\n\
    1.37 -        \|> add_thyname " ^ quote thy_name ^ ";\n\
    1.38 +        \|> Theory.add_name " ^ quote thy_name ^ ";\n\
    1.39          \\n\
    1.40          \val _ = store_theory (thy, " ^ quote thy_name ^ ");\n\
    1.41          \\n\
    1.42 @@ -534,16 +534,16 @@
    1.43  
    1.44  val pure_sections =
    1.45   [section "oracle" "|> set_oracle" (name >> strip_quotes),
    1.46 -  section "classes" "|> add_classes" class_decls,
    1.47 -  section "default" "|> add_defsort" sort,
    1.48 +  section "classes" "|> Theory.add_classes" class_decls,
    1.49 +  section "default" "|> Theory.add_defsort" sort,
    1.50    section "types" "" type_decls,
    1.51 -  section "arities" "|> add_arities" arity_decls,
    1.52 -  section "consts" "|> add_consts" const_decls,
    1.53 -  section "syntax" "|> add_modesyntax" syntax_decls,
    1.54 -  section "translations" "|> add_trrules" trans_decls,
    1.55 -  axm_section "rules" "|> add_axioms" axiom_decls,
    1.56 -  axm_section "defs" "|> add_defs" axiom_decls,
    1.57 -  axm_section "constdefs" "|> add_consts" constaxiom_decls,
    1.58 +  section "arities" "|> Theory.add_arities" arity_decls,
    1.59 +  section "consts" "|> Theory.add_consts" const_decls,
    1.60 +  section "syntax" "|> Theory.add_modesyntax" syntax_decls,
    1.61 +  section "translations" "|> Theory.add_trrules" trans_decls,
    1.62 +  axm_section "rules" "|> Theory.add_axioms" axiom_decls,
    1.63 +  axm_section "defs" "|> Theory.add_defs" axiom_decls,
    1.64 +  axm_section "constdefs" "|> Theory.add_consts" constaxiom_decls,
    1.65    axm_section "axclass" "|> AxClass.add_axclass" axclass_decl,
    1.66    section "instance" "" instance_decl];
    1.67