src/Pure/theory.ML

--- a/src/Pure/theory.ML	Sat Oct 24 19:24:50 2009 +0200
+++ b/src/Pure/theory.ML	Sat Oct 24 19:47:37 2009 +0200
@@ -19,7 +19,7 @@
   val checkpoint: theory -> theory
   val copy: theory -> theory
   val requires: theory -> string -> string -> unit
-  val axiom_space: theory -> NameSpace.T
+  val axiom_space: theory -> Name_Space.T
   val axiom_table: theory -> term Symtab.table
   val axioms_of: theory -> (string * term) list
   val all_axioms_of: theory -> (string * term) list
@@ -80,7 +80,7 @@
   perhaps (perhaps_loop (perhaps_apply (map fst wrappers)));
 
 datatype thy = Thy of
- {axioms: term NameSpace.table,
+ {axioms: term Name_Space.table,
   defs: Defs.T,
   wrappers: wrapper list * wrapper list};
 
@@ -89,18 +89,18 @@
 structure ThyData = TheoryDataFun
 (
   type T = thy;
-  val empty = make_thy (NameSpace.empty_table, Defs.empty, ([], []));
+  val empty = make_thy (Name_Space.empty_table, Defs.empty, ([], []));
   val copy = I;
 
   fun extend (Thy {axioms = _, defs, wrappers}) =
-    make_thy (NameSpace.empty_table, defs, wrappers);
+    make_thy (Name_Space.empty_table, defs, wrappers);
 
   fun merge pp (thy1, thy2) =
     let
       val Thy {axioms = _, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
       val Thy {axioms = _, defs = defs2, wrappers = (bgs2, ens2)} = thy2;
 
-      val axioms' = NameSpace.empty_table;
+      val axioms' = Name_Space.empty_table;
       val defs' = Defs.merge pp (defs1, defs2);
       val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2);
       val ens' = Library.merge (eq_snd op =) (ens1, ens2);
@@ -174,7 +174,7 @@
 fun gen_add_axioms prep_axm raw_axms thy = thy |> map_axioms (fn axioms =>
   let
     val axms = map (apsnd Logic.varify o prep_axm thy) raw_axms;
-    val axioms' = fold (#2 oo NameSpace.define true (Sign.naming_of thy)) axms axioms;
+    val axioms' = fold (#2 oo Name_Space.define true (Sign.naming_of thy)) axms axioms;
   in axioms' end);
 
 in