fully qualified names: Theory.add_XXX;

--- a/src/Pure/Thy/thy_parse.ML	Wed Oct 01 17:36:51 1997 +0200
+++ b/src/Pure/Thy/thy_parse.ML	Wed Oct 01 17:40:09 1997 +0200
@@ -279,8 +279,8 @@
       [(parens (commas [t, mk_list xs, rhs, syn]), true)];
 
 fun mk_type_decls tys =
-  "|> add_types\n" ^ mk_big_list (keyfilter tys false) ^ "\n\n\
-  \|> add_tyabbrs\n" ^ mk_big_list (keyfilter tys true);
+  "|> Theory.add_types\n" ^ mk_big_list (keyfilter tys false) ^ "\n\n\
+  \|> Theory.add_tyabbrs\n" ^ mk_big_list (keyfilter tys true);
 
 
 val old_type_decl = names1 -- nat -- opt_infix >> mk_old_type_decl;
@@ -362,7 +362,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|> add_defs\n" ^ axms_defs, axms_names)
+       "\n\n|> Theory.add_defs\n" ^ axms_defs, axms_names)
   end;
 
 val constaxiom_decls =
@@ -470,14 +470,14 @@
         \\n\
         \val thy = thy\n\
         \\n\
-        \|> add_trfuns\n"
+        \|> Theory.add_trfuns\n"
         ^ trfun_args ^ "\n\
-        \|> add_trfunsT typed_print_translation \n\
-        \|> add_tokentrfuns token_translation \n\
+        \|> Theory.add_trfunsT typed_print_translation \n\
+        \|> Theory.add_tokentrfuns token_translation \n\
         \\n"
         ^ extxt ^ "\n\
         \\n\
-        \|> add_thyname " ^ quote thy_name ^ ";\n\
+        \|> Theory.add_name " ^ quote thy_name ^ ";\n\
         \\n\
         \val _ = store_theory (thy, " ^ quote thy_name ^ ");\n\
         \\n\
@@ -534,16 +534,16 @@
 
 val pure_sections =
  [section "oracle" "|> set_oracle" (name >> strip_quotes),
-  section "classes" "|> add_classes" class_decls,
-  section "default" "|> add_defsort" sort,
+  section "classes" "|> Theory.add_classes" class_decls,
+  section "default" "|> Theory.add_defsort" sort,
   section "types" "" type_decls,
-  section "arities" "|> add_arities" arity_decls,
-  section "consts" "|> add_consts" const_decls,
-  section "syntax" "|> add_modesyntax" syntax_decls,
-  section "translations" "|> add_trrules" trans_decls,
-  axm_section "rules" "|> add_axioms" axiom_decls,
-  axm_section "defs" "|> add_defs" axiom_decls,
-  axm_section "constdefs" "|> add_consts" constaxiom_decls,
+  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" "|> Theory.add_axioms" axiom_decls,
+  axm_section "defs" "|> Theory.add_defs" axiom_decls,
+  axm_section "constdefs" "|> Theory.add_consts" constaxiom_decls,
   axm_section "axclass" "|> AxClass.add_axclass" axclass_decl,
   section "instance" "" instance_decl];
 

--- a/src/Pure/axclass.ML	Wed Oct 01 17:36:51 1997 +0200
+++ b/src/Pure/axclass.ML	Wed Oct 01 17:40:09 1997 +0200
@@ -124,7 +124,7 @@
 
 (*general theorems*)
 fun add_thms_as_axms thms thy =
-  add_axioms_i (map (apsnd (prep_thm_axm thy)) thms) thy;
+  Theory.add_axioms_i (map (apsnd (prep_thm_axm thy)) thms) thy;
 
 (*theorems expressing class relations*)
 fun add_classrel_thms thms thy =
@@ -136,7 +136,7 @@
           raise THM ("add_classrel_thms: theorem is not a class relation", 0, [thm]);
       in (c1, c2) end;
   in
-    add_classrel (map prep_thm thms) thy
+    Theory.add_classrel (map prep_thm thms) thy
   end;
 
 (*theorems expressing arities*)
@@ -149,7 +149,7 @@
           raise THM ("add_arity_thms: theorem is not an arity", 0, [thm]);
       in (t, ss, [c]) end;
   in
-    add_arities (map prep_thm thms) thy
+    Theory.add_arities (map prep_thm thms) thy
   end;
 
 
@@ -173,7 +173,7 @@
 fun ext_axclass prep_axm (class, super_classes) raw_axioms old_thy =
   let
     val axioms = map (prep_axm (sign_of old_thy)) raw_axioms;
-    val thy = add_classes [(class, super_classes)] old_thy;
+    val thy = Theory.add_classes [(class, super_classes)] old_thy;
     val sign = sign_of thy;
 
 
@@ -210,7 +210,7 @@
     val intro_axm = Logic.list_implies
       (map inclass super_classes @ map (int_axm o snd) axioms, inclass class);
   in
-    add_axioms_i ((class ^ "I", intro_axm) :: abs_axioms) thy
+    Theory.add_axioms_i ((class ^ "I", intro_axm) :: abs_axioms) thy
   end;