src/Pure/sign.ML
changeset 42359 6ca5407863ed
parent 42358 b47d41d9f4b5
child 42360 da8817d01e7c
     1.1 --- a/src/Pure/sign.ML	Sat Apr 16 13:48:45 2011 +0200
     1.2 +++ b/src/Pure/sign.ML	Sat Apr 16 15:25:25 2011 +0200
     1.3 @@ -49,15 +49,12 @@
     1.4    val class_space: theory -> Name_Space.T
     1.5    val type_space: theory -> Name_Space.T
     1.6    val const_space: theory -> Name_Space.T
     1.7 +  val intern_class: theory -> xstring -> string
     1.8 +  val intern_type: theory -> xstring -> string
     1.9 +  val intern_const: theory -> xstring -> string
    1.10    val class_alias: binding -> class -> theory -> theory
    1.11    val type_alias: binding -> string -> theory -> theory
    1.12    val const_alias: binding -> string -> theory -> theory
    1.13 -  val intern_class: theory -> xstring -> string
    1.14 -  val extern_class: theory -> string -> xstring
    1.15 -  val intern_type: theory -> xstring -> string
    1.16 -  val extern_type: theory -> string -> xstring
    1.17 -  val intern_const: theory -> xstring -> string
    1.18 -  val extern_const: theory -> string -> xstring
    1.19    val arity_number: theory -> string -> int
    1.20    val arity_sorts: theory -> string -> sort -> sort list
    1.21    val certify_class: theory -> class -> class
    1.22 @@ -222,23 +219,20 @@
    1.23  
    1.24  
    1.25  
    1.26 -(** intern / extern names **)
    1.27 +(** name spaces **)
    1.28  
    1.29  val class_space = Type.class_space o tsig_of;
    1.30  val type_space = Type.type_space o tsig_of;
    1.31  val const_space = Consts.space_of o consts_of;
    1.32  
    1.33 +val intern_class = Name_Space.intern o class_space;
    1.34 +val intern_type = Name_Space.intern o type_space;
    1.35 +val intern_const = Name_Space.intern o const_space;
    1.36 +
    1.37  fun class_alias b c thy = map_tsig (Type.class_alias (naming_of thy) b c) thy;
    1.38  fun type_alias b c thy = map_tsig (Type.type_alias (naming_of thy) b c) thy;
    1.39  fun const_alias b c thy = map_consts (Consts.alias (naming_of thy) b c) thy;
    1.40  
    1.41 -val intern_class = Name_Space.intern o class_space;
    1.42 -fun extern_class thy = Name_Space.extern (ProofContext.init_global thy) (class_space thy);
    1.43 -val intern_type = Name_Space.intern o type_space;
    1.44 -fun extern_type thy = Name_Space.extern (ProofContext.init_global thy) (type_space thy);
    1.45 -val intern_const = Name_Space.intern o const_space;
    1.46 -fun extern_const thy = Name_Space.extern (ProofContext.init_global thy) (const_space thy);
    1.47 -
    1.48  
    1.49  
    1.50  (** certify entities **)    (*exception TYPE*)