src/Pure/sign.ML
changeset 33095 bbd52d2f8696
parent 32789 d89327de0b3c
child 33097 9d501e11084a
     1.1 --- a/src/Pure/sign.ML	Sat Oct 24 19:24:50 2009 +0200
     1.2 +++ b/src/Pure/sign.ML	Sat Oct 24 19:47:37 2009 +0200
     1.3 @@ -8,11 +8,11 @@
     1.4  signature SIGN =
     1.5  sig
     1.6    val rep_sg: theory ->
     1.7 -   {naming: NameSpace.naming,
     1.8 +   {naming: Name_Space.naming,
     1.9      syn: Syntax.syntax,
    1.10      tsig: Type.tsig,
    1.11      consts: Consts.T}
    1.12 -  val naming_of: theory -> NameSpace.naming
    1.13 +  val naming_of: theory -> Name_Space.naming
    1.14    val full_name: theory -> binding -> string
    1.15    val full_name_path: theory -> string -> binding -> string
    1.16    val full_bname: theory -> bstring -> string
    1.17 @@ -44,9 +44,9 @@
    1.18    val const_typargs: theory -> string * typ -> typ list
    1.19    val const_instance: theory -> string * typ list -> typ
    1.20    val mk_const: theory -> string * typ list -> term
    1.21 -  val class_space: theory -> NameSpace.T
    1.22 -  val type_space: theory -> NameSpace.T
    1.23 -  val const_space: theory -> NameSpace.T
    1.24 +  val class_space: theory -> Name_Space.T
    1.25 +  val type_space: theory -> Name_Space.T
    1.26 +  val const_space: theory -> Name_Space.T
    1.27    val intern_class: theory -> xstring -> string
    1.28    val extern_class: theory -> string -> xstring
    1.29    val intern_type: theory -> xstring -> string
    1.30 @@ -137,7 +137,7 @@
    1.31  (** datatype sign **)
    1.32  
    1.33  datatype sign = Sign of
    1.34 - {naming: NameSpace.naming,     (*common naming conventions*)
    1.35 + {naming: Name_Space.naming,    (*common naming conventions*)
    1.36    syn: Syntax.syntax,           (*concrete syntax for terms, types, sorts*)
    1.37    tsig: Type.tsig,              (*order-sorted signature of types*)
    1.38    consts: Consts.T};            (*polymorphic constants*)
    1.39 @@ -150,17 +150,17 @@
    1.40    type T = sign;
    1.41    val copy = I;
    1.42    fun extend (Sign {syn, tsig, consts, ...}) =
    1.43 -    make_sign (NameSpace.default_naming, syn, tsig, consts);
    1.44 +    make_sign (Name_Space.default_naming, syn, tsig, consts);
    1.45  
    1.46    val empty =
    1.47 -    make_sign (NameSpace.default_naming, Syntax.basic_syn, Type.empty_tsig, Consts.empty);
    1.48 +    make_sign (Name_Space.default_naming, Syntax.basic_syn, Type.empty_tsig, Consts.empty);
    1.49  
    1.50    fun merge pp (sign1, sign2) =
    1.51      let
    1.52        val Sign {naming = _, syn = syn1, tsig = tsig1, consts = consts1} = sign1;
    1.53        val Sign {naming = _, syn = syn2, tsig = tsig2, consts = consts2} = sign2;
    1.54  
    1.55 -      val naming = NameSpace.default_naming;
    1.56 +      val naming = Name_Space.default_naming;
    1.57        val syn = Syntax.merge_syntaxes syn1 syn2;
    1.58        val tsig = Type.merge_tsigs pp (tsig1, tsig2);
    1.59        val consts = Consts.merge (consts1, consts2);
    1.60 @@ -182,10 +182,10 @@
    1.61  
    1.62  val naming_of = #naming o rep_sg;
    1.63  
    1.64 -val full_name = NameSpace.full_name o naming_of;
    1.65 -fun full_name_path thy path = NameSpace.full_name (NameSpace.add_path path (naming_of thy));
    1.66 +val full_name = Name_Space.full_name o naming_of;
    1.67 +fun full_name_path thy path = Name_Space.full_name (Name_Space.add_path path (naming_of thy));
    1.68  
    1.69 -fun full_bname thy = NameSpace.full_name (naming_of thy) o Binding.name;
    1.70 +fun full_bname thy = Name_Space.full_name (naming_of thy) o Binding.name;
    1.71  fun full_bname_path thy path = full_name_path thy path o Binding.name;
    1.72  
    1.73  
    1.74 @@ -240,12 +240,12 @@
    1.75  val type_space = #1 o #types o Type.rep_tsig o tsig_of;
    1.76  val const_space = Consts.space_of o consts_of;
    1.77  
    1.78 -val intern_class = NameSpace.intern o class_space;
    1.79 -val extern_class = NameSpace.extern o class_space;
    1.80 -val intern_type = NameSpace.intern o type_space;
    1.81 -val extern_type = NameSpace.extern o type_space;
    1.82 -val intern_const = NameSpace.intern o const_space;
    1.83 -val extern_const = NameSpace.extern o const_space;
    1.84 +val intern_class = Name_Space.intern o class_space;
    1.85 +val extern_class = Name_Space.extern o class_space;
    1.86 +val intern_type = Name_Space.intern o type_space;
    1.87 +val extern_type = Name_Space.extern o type_space;
    1.88 +val intern_const = Name_Space.intern o const_space;
    1.89 +val extern_const = Name_Space.extern o const_space;
    1.90  
    1.91  val intern_sort = map o intern_class;
    1.92  val extern_sort = map o extern_class;
    1.93 @@ -612,10 +612,10 @@
    1.94  
    1.95  (* naming *)
    1.96  
    1.97 -val add_path = map_naming o NameSpace.add_path;
    1.98 -val root_path = map_naming NameSpace.root_path;
    1.99 -val parent_path = map_naming NameSpace.parent_path;
   1.100 -val mandatory_path = map_naming o NameSpace.mandatory_path;
   1.101 +val add_path = map_naming o Name_Space.add_path;
   1.102 +val root_path = map_naming Name_Space.root_path;
   1.103 +val parent_path = map_naming Name_Space.parent_path;
   1.104 +val mandatory_path = map_naming o Name_Space.mandatory_path;
   1.105  
   1.106  fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
   1.107