unused;
authorwenzelm
Mon Jul 03 09:12:13 2017 +0200 (2017-07-03)
changeset 66245da3b0e848182
parent 66243 453f9cabddb5
child 66246 c2c18b6b48da
unused;
src/Pure/Isar/local_theory.ML
src/Pure/Isar/proof_context.ML
src/Pure/sign.ML
src/Pure/type.ML
     1.1 --- a/src/Pure/Isar/local_theory.ML	Sat Jul 01 16:39:56 2017 +0200
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Mon Jul 03 09:12:13 2017 +0200
     1.3 @@ -63,7 +63,6 @@
     1.4    val set_defsort: sort -> local_theory -> local_theory
     1.5    val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
     1.6    val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
     1.7 -  val class_alias: binding -> class -> local_theory -> local_theory
     1.8    val type_alias: binding -> string -> local_theory -> local_theory
     1.9    val const_alias: binding -> string -> local_theory -> local_theory
    1.10    val init: Name_Space.naming -> operations -> Proof.context -> local_theory
    1.11 @@ -335,7 +334,6 @@
    1.12      let val b' = Morphism.binding phi b
    1.13      in Context.mapping (global_alias b' name) (local_alias b' name) end);
    1.14  
    1.15 -val class_alias = syntax_alias Sign.class_alias Proof_Context.class_alias;
    1.16  val type_alias = syntax_alias Sign.type_alias Proof_Context.type_alias;
    1.17  val const_alias = syntax_alias Sign.const_alias Proof_Context.const_alias;
    1.18  
     2.1 --- a/src/Pure/Isar/proof_context.ML	Sat Jul 01 16:39:56 2017 +0200
     2.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Jul 03 09:12:13 2017 +0200
     2.3 @@ -158,7 +158,6 @@
     2.4      Context.generic -> Context.generic
     2.5    val generic_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism ->
     2.6      Context.generic -> Context.generic
     2.7 -  val class_alias: binding -> class -> Proof.context -> Proof.context
     2.8    val type_alias: binding -> string -> Proof.context -> Proof.context
     2.9    val const_alias: binding -> string -> Proof.context -> Proof.context
    2.10    val fact_alias: binding -> string -> Proof.context -> Proof.context
    2.11 @@ -1184,7 +1183,6 @@
    2.12  
    2.13  (* aliases *)
    2.14  
    2.15 -fun class_alias b c ctxt = (map_tsig o apfst) (Type.class_alias (naming_of ctxt) b c) ctxt;
    2.16  fun type_alias b c ctxt = (map_tsig o apfst) (Type.type_alias (naming_of ctxt) b c) ctxt;
    2.17  fun const_alias b c ctxt = (map_consts o apfst) (Consts.alias (naming_of ctxt) b c) ctxt;
    2.18  fun fact_alias b c ctxt = map_facts (Facts.alias (naming_of ctxt) b c) ctxt;
     3.1 --- a/src/Pure/sign.ML	Sat Jul 01 16:39:56 2017 +0200
     3.2 +++ b/src/Pure/sign.ML	Mon Jul 03 09:12:13 2017 +0200
     3.3 @@ -53,7 +53,6 @@
     3.4    val intern_class: theory -> xstring -> string
     3.5    val intern_type: theory -> xstring -> string
     3.6    val intern_const: theory -> xstring -> string
     3.7 -  val class_alias: binding -> class -> theory -> theory
     3.8    val type_alias: binding -> string -> theory -> theory
     3.9    val const_alias: binding -> string -> theory -> theory
    3.10    val arity_number: theory -> string -> int
    3.11 @@ -246,7 +245,6 @@
    3.12  val intern_type = Name_Space.intern o type_space;
    3.13  val intern_const = Name_Space.intern o const_space;
    3.14  
    3.15 -fun class_alias b c thy = map_tsig (Type.class_alias (naming_of thy) b c) thy;
    3.16  fun type_alias b c thy = map_tsig (Type.type_alias (naming_of thy) b c) thy;
    3.17  fun const_alias b c thy = map_consts (Consts.alias (naming_of thy) b c) thy;
    3.18  
     4.1 --- a/src/Pure/type.ML	Sat Jul 01 16:39:56 2017 +0200
     4.2 +++ b/src/Pure/type.ML	Mon Jul 03 09:12:13 2017 +0200
     4.3 @@ -29,7 +29,6 @@
     4.4    val change_ignore: tsig -> tsig
     4.5    val empty_tsig: tsig
     4.6    val class_space: tsig -> Name_Space.T
     4.7 -  val class_alias: Name_Space.naming -> binding -> string -> tsig -> tsig
     4.8    val defaultS: tsig -> sort
     4.9    val logical_types: tsig -> string list
    4.10    val eq_sort: tsig -> sort * sort -> bool
    4.11 @@ -202,9 +201,6 @@
    4.12  
    4.13  val class_space = #1 o #classes o rep_tsig;
    4.14  
    4.15 -fun class_alias naming binding name = map_tsig (fn ((space, classes), default, types) =>
    4.16 -  ((Name_Space.alias naming binding name space, classes), default, types));
    4.17 -
    4.18  fun defaultS (TSig {default, ...}) = default;
    4.19  fun logical_types (TSig {log_types, ...}) = log_types;
    4.20