unused;
authorwenzelm
Sun Mar 09 17:43:40 2014 +0100 (2014-03-09)
changeset 560082897b2a4f7fd
parent 56007 1b61dfbcf9a4
child 56009 dda076a32aea
unused;
src/Pure/consts.ML
src/Pure/type.ML
     1.1 --- a/src/Pure/consts.ML	Sun Mar 09 17:40:02 2014 +0100
     1.2 +++ b/src/Pure/consts.ML	Sun Mar 09 17:43:40 2014 +0100
     1.3 @@ -22,9 +22,7 @@
     1.4    val alias: Name_Space.naming -> binding -> string -> T -> T
     1.5    val is_concealed: T -> string -> bool
     1.6    val intern: T -> xstring -> string
     1.7 -  val extern: Proof.context -> T -> string -> xstring
     1.8    val intern_syntax: T -> xstring -> string
     1.9 -  val extern_syntax: Proof.context -> T -> string -> xstring
    1.10    val check_const: Context.generic -> T -> xstring * Position.T list -> term * Position.report list
    1.11    val certify: Context.pretty -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
    1.12    val typargs: T -> string * typ -> typ list
    1.13 @@ -128,18 +126,12 @@
    1.14  val is_concealed = Name_Space.is_concealed o space_of;
    1.15  
    1.16  val intern = Name_Space.intern o space_of;
    1.17 -fun extern ctxt = Name_Space.extern ctxt o space_of;
    1.18  
    1.19  fun intern_syntax consts s =
    1.20    (case try Lexicon.unmark_const s of
    1.21      SOME c => c
    1.22    | NONE => intern consts s);
    1.23  
    1.24 -fun extern_syntax ctxt consts s =
    1.25 -  (case try Lexicon.unmark_const s of
    1.26 -    SOME c => extern ctxt consts c
    1.27 -  | NONE => s);
    1.28 -
    1.29  
    1.30  (* check_const *)
    1.31  
     2.1 --- a/src/Pure/type.ML	Sun Mar 09 17:40:02 2014 +0100
     2.2 +++ b/src/Pure/type.ML	Sun Mar 09 17:43:40 2014 +0100
     2.3 @@ -28,8 +28,6 @@
     2.4    val empty_tsig: tsig
     2.5    val class_space: tsig -> Name_Space.T
     2.6    val class_alias: Name_Space.naming -> binding -> string -> tsig -> tsig
     2.7 -  val intern_class: tsig -> xstring -> string
     2.8 -  val extern_class: Proof.context -> tsig -> string -> xstring
     2.9    val defaultS: tsig -> sort
    2.10    val logical_types: tsig -> string list
    2.11    val eq_sort: tsig -> sort * sort -> bool
    2.12 @@ -49,8 +47,6 @@
    2.13    val restore_mode: Proof.context -> Proof.context -> Proof.context
    2.14    val type_space: tsig -> Name_Space.T
    2.15    val type_alias: Name_Space.naming -> binding -> string -> tsig -> tsig
    2.16 -  val intern_type: tsig -> xstring -> string
    2.17 -  val extern_type: Proof.context -> tsig -> string -> xstring
    2.18    val is_logtype: tsig -> string -> bool
    2.19    val check_decl: Context.generic -> tsig ->
    2.20      xstring * Position.T -> (string * Position.report list) * decl
    2.21 @@ -200,9 +196,6 @@
    2.22  fun class_alias naming binding name = map_tsig (fn ((space, classes), default, types) =>
    2.23    ((Name_Space.alias naming binding name space, classes), default, types));
    2.24  
    2.25 -val intern_class = Name_Space.intern o class_space;
    2.26 -fun extern_class ctxt = Name_Space.extern ctxt o class_space;
    2.27 -
    2.28  fun defaultS (TSig {default, ...}) = default;
    2.29  fun logical_types (TSig {log_types, ...}) = log_types;
    2.30  
    2.31 @@ -249,9 +242,6 @@
    2.32  fun type_alias naming binding name = map_tsig (fn (classes, default, (space, types)) =>
    2.33    (classes, default, (Name_Space.alias naming binding name space, types)));
    2.34  
    2.35 -val intern_type = Name_Space.intern o type_space;
    2.36 -fun extern_type ctxt = Name_Space.extern ctxt o type_space;
    2.37 -
    2.38  val is_logtype = member (op =) o logical_types;
    2.39  
    2.40