src/Pure/consts.ML

--- a/src/Pure/consts.ML	Sat Oct 24 19:24:50 2009 +0200
+++ b/src/Pure/consts.ML	Sat Oct 24 19:47:37 2009 +0200
@@ -11,15 +11,15 @@
   val eq_consts: T * T -> bool
   val retrieve_abbrevs: T -> string list -> term -> (term * term) list
   val dest: T ->
-   {constants: (typ * term option) NameSpace.table,
-    constraints: typ NameSpace.table}
+   {constants: (typ * term option) Name_Space.table,
+    constraints: typ Name_Space.table}
   val the_type: T -> string -> typ                             (*exception TYPE*)
   val the_abbreviation: T -> string -> typ * term              (*exception TYPE*)
   val type_scheme: T -> string -> typ                          (*exception TYPE*)
   val the_tags: T -> string -> Properties.T                    (*exception TYPE*)
   val is_monomorphic: T -> string -> bool                      (*exception TYPE*)
   val the_constraint: T -> string -> typ                       (*exception TYPE*)
-  val space_of: T -> NameSpace.T
+  val space_of: T -> Name_Space.T
   val intern: T -> xstring -> string
   val extern: T -> string -> xstring
   val extern_early: T -> string -> xstring
@@ -29,9 +29,9 @@
   val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
   val typargs: T -> string * typ -> typ list
   val instance: T -> string * typ list -> typ
-  val declare: bool -> NameSpace.naming -> Properties.T -> (binding * typ) -> T -> T
+  val declare: bool -> Name_Space.naming -> Properties.T -> (binding * typ) -> T -> T
   val constrain: string * typ option -> T -> T
-  val abbreviate: Pretty.pp -> Type.tsig -> NameSpace.naming -> string -> Properties.T ->
+  val abbreviate: Pretty.pp -> Type.tsig -> Name_Space.naming -> string -> Properties.T ->
     binding * term -> T -> (term * term) * T
   val revert_abbrev: string -> string -> T -> T
   val hide: bool -> string -> T -> T
@@ -50,7 +50,7 @@
 type abbrev = {rhs: term, normal_rhs: term, force_expand: bool};
 
 datatype T = Consts of
- {decls: (decl * abbrev option) NameSpace.table,
+ {decls: (decl * abbrev option) Name_Space.table,
   constraints: typ Symtab.table,
   rev_abbrevs: (term * term) Item_Net.T Symtab.table};
 
@@ -123,8 +123,8 @@
 
 fun space_of (Consts {decls = (space, _), ...}) = space;
 
-val intern = NameSpace.intern o space_of;
-val extern = NameSpace.extern o space_of;
+val intern = Name_Space.intern o space_of;
+val extern = Name_Space.extern o space_of;
 
 fun extern_early consts c =
   (case try (the_const consts) c of
@@ -224,7 +224,7 @@
 (* name space *)
 
 fun hide fully c = map_consts (fn (decls, constraints, rev_abbrevs) =>
-  (apfst (NameSpace.hide fully c) decls, constraints, rev_abbrevs));
+  (apfst (Name_Space.hide fully c) decls, constraints, rev_abbrevs));
 
 
 (* declarations *)
@@ -234,7 +234,7 @@
     let
       val tags' = tags |> Position.default_properties (Position.thread_data ());
       val decl = {T = declT, typargs = typargs_of declT, tags = tags', authentic = authentic};
-      val (_, decls') = decls |> NameSpace.define true naming (b, (decl, NONE));
+      val (_, decls') = decls |> Name_Space.define true naming (b, (decl, NONE));
     in (decls', constraints, rev_abbrevs) end);
 
 
@@ -280,7 +280,7 @@
       |> Term.close_schematic_term;
     val normal_rhs = expand_term rhs;
     val T = Term.fastype_of rhs;
-    val lhs = Const (NameSpace.full_name naming b, T);
+    val lhs = Const (Name_Space.full_name naming b, T);
   in
     consts |> map_consts (fn (decls, constraints, rev_abbrevs) =>
       let
@@ -288,7 +288,7 @@
         val decl = {T = T, typargs = typargs_of T, tags = tags', authentic = true};
         val abbr = {rhs = rhs, normal_rhs = normal_rhs, force_expand = force_expand};
         val (_, decls') = decls
-          |> NameSpace.define true naming (b, (decl, SOME abbr));
+          |> Name_Space.define true naming (b, (decl, SOME abbr));
         val rev_abbrevs' = rev_abbrevs
           |> insert_abbrevs mode (rev_abbrev lhs rhs);
       in (decls', constraints, rev_abbrevs') end)
@@ -307,13 +307,13 @@
 
 (* empty and merge *)
 
-val empty = make_consts (NameSpace.empty_table, Symtab.empty, Symtab.empty);
+val empty = make_consts (Name_Space.empty_table, Symtab.empty, Symtab.empty);
 
 fun merge
    (Consts {decls = decls1, constraints = constraints1, rev_abbrevs = rev_abbrevs1},
     Consts {decls = decls2, constraints = constraints2, rev_abbrevs = rev_abbrevs2}) =
   let
-    val decls' = NameSpace.merge_tables (decls1, decls2);
+    val decls' = Name_Space.merge_tables (decls1, decls2);
     val constraints' = Symtab.join (K fst) (constraints1, constraints2);
     val rev_abbrevs' = Symtab.join (K Item_Net.merge) (rev_abbrevs1, rev_abbrevs2);
   in make_consts (decls', constraints', rev_abbrevs') end;