src/Pure/type.ML
changeset 56008 2897b2a4f7fd
parent 55956 94d384d621b0
child 56025 d74fed45fa8b
     1.1 --- a/src/Pure/type.ML	Sun Mar 09 17:40:02 2014 +0100
     1.2 +++ b/src/Pure/type.ML	Sun Mar 09 17:43:40 2014 +0100
     1.3 @@ -28,8 +28,6 @@
     1.4    val empty_tsig: tsig
     1.5    val class_space: tsig -> Name_Space.T
     1.6    val class_alias: Name_Space.naming -> binding -> string -> tsig -> tsig
     1.7 -  val intern_class: tsig -> xstring -> string
     1.8 -  val extern_class: Proof.context -> tsig -> string -> xstring
     1.9    val defaultS: tsig -> sort
    1.10    val logical_types: tsig -> string list
    1.11    val eq_sort: tsig -> sort * sort -> bool
    1.12 @@ -49,8 +47,6 @@
    1.13    val restore_mode: Proof.context -> Proof.context -> Proof.context
    1.14    val type_space: tsig -> Name_Space.T
    1.15    val type_alias: Name_Space.naming -> binding -> string -> tsig -> tsig
    1.16 -  val intern_type: tsig -> xstring -> string
    1.17 -  val extern_type: Proof.context -> tsig -> string -> xstring
    1.18    val is_logtype: tsig -> string -> bool
    1.19    val check_decl: Context.generic -> tsig ->
    1.20      xstring * Position.T -> (string * Position.report list) * decl
    1.21 @@ -200,9 +196,6 @@
    1.22  fun class_alias naming binding name = map_tsig (fn ((space, classes), default, types) =>
    1.23    ((Name_Space.alias naming binding name space, classes), default, types));
    1.24  
    1.25 -val intern_class = Name_Space.intern o class_space;
    1.26 -fun extern_class ctxt = Name_Space.extern ctxt o class_space;
    1.27 -
    1.28  fun defaultS (TSig {default, ...}) = default;
    1.29  fun logical_types (TSig {log_types, ...}) = log_types;
    1.30  
    1.31 @@ -249,9 +242,6 @@
    1.32  fun type_alias naming binding name = map_tsig (fn (classes, default, (space, types)) =>
    1.33    (classes, default, (Name_Space.alias naming binding name space, types)));
    1.34  
    1.35 -val intern_type = Name_Space.intern o type_space;
    1.36 -fun extern_type ctxt = Name_Space.extern ctxt o type_space;
    1.37 -
    1.38  val is_logtype = member (op =) o logical_types;
    1.39  
    1.40