fully qualified names: Theory.add_XXX;
authorwenzelm
Wed Oct 01 17:40:09 1997 +0200 (1997-10-01)
changeset 3764fe7719aee219
parent 3763 31ec17820f49
child 3765 6a4f3b976db3
fully qualified names: Theory.add_XXX;
src/Pure/Thy/thy_parse.ML
src/Pure/axclass.ML
     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  
     2.1 --- a/src/Pure/axclass.ML	Wed Oct 01 17:36:51 1997 +0200
     2.2 +++ b/src/Pure/axclass.ML	Wed Oct 01 17:40:09 1997 +0200
     2.3 @@ -124,7 +124,7 @@
     2.4  
     2.5  (*general theorems*)
     2.6  fun add_thms_as_axms thms thy =
     2.7 -  add_axioms_i (map (apsnd (prep_thm_axm thy)) thms) thy;
     2.8 +  Theory.add_axioms_i (map (apsnd (prep_thm_axm thy)) thms) thy;
     2.9  
    2.10  (*theorems expressing class relations*)
    2.11  fun add_classrel_thms thms thy =
    2.12 @@ -136,7 +136,7 @@
    2.13            raise THM ("add_classrel_thms: theorem is not a class relation", 0, [thm]);
    2.14        in (c1, c2) end;
    2.15    in
    2.16 -    add_classrel (map prep_thm thms) thy
    2.17 +    Theory.add_classrel (map prep_thm thms) thy
    2.18    end;
    2.19  
    2.20  (*theorems expressing arities*)
    2.21 @@ -149,7 +149,7 @@
    2.22            raise THM ("add_arity_thms: theorem is not an arity", 0, [thm]);
    2.23        in (t, ss, [c]) end;
    2.24    in
    2.25 -    add_arities (map prep_thm thms) thy
    2.26 +    Theory.add_arities (map prep_thm thms) thy
    2.27    end;
    2.28  
    2.29  
    2.30 @@ -173,7 +173,7 @@
    2.31  fun ext_axclass prep_axm (class, super_classes) raw_axioms old_thy =
    2.32    let
    2.33      val axioms = map (prep_axm (sign_of old_thy)) raw_axioms;
    2.34 -    val thy = add_classes [(class, super_classes)] old_thy;
    2.35 +    val thy = Theory.add_classes [(class, super_classes)] old_thy;
    2.36      val sign = sign_of thy;
    2.37  
    2.38  
    2.39 @@ -210,7 +210,7 @@
    2.40      val intro_axm = Logic.list_implies
    2.41        (map inclass super_classes @ map (int_axm o snd) axioms, inclass class);
    2.42    in
    2.43 -    add_axioms_i ((class ^ "I", intro_axm) :: abs_axioms) thy
    2.44 +    Theory.add_axioms_i ((class ^ "I", intro_axm) :: abs_axioms) thy
    2.45    end;
    2.46  
    2.47