# HG changeset patch
# User wenzelm
# Date 1499065933 -7200
# Node ID da3b0e848182d05c7dfd5be6ab16fdc8240caec0
# Parent  453f9cabddb5a13f9151de350dd53e39cb953f22
unused;

diff -r 453f9cabddb5 -r da3b0e848182 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Sat Jul 01 16:39:56 2017 +0200
+++ b/src/Pure/Isar/local_theory.ML	Mon Jul 03 09:12:13 2017 +0200
@@ -63,7 +63,6 @@
   val set_defsort: sort -> local_theory -> local_theory
   val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
-  val class_alias: binding -> class -> local_theory -> local_theory
   val type_alias: binding -> string -> local_theory -> local_theory
   val const_alias: binding -> string -> local_theory -> local_theory
   val init: Name_Space.naming -> operations -> Proof.context -> local_theory
@@ -335,7 +334,6 @@
     let val b' = Morphism.binding phi b
     in Context.mapping (global_alias b' name) (local_alias b' name) end);
 
-val class_alias = syntax_alias Sign.class_alias Proof_Context.class_alias;
 val type_alias = syntax_alias Sign.type_alias Proof_Context.type_alias;
 val const_alias = syntax_alias Sign.const_alias Proof_Context.const_alias;
 
diff -r 453f9cabddb5 -r da3b0e848182 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat Jul 01 16:39:56 2017 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Jul 03 09:12:13 2017 +0200
@@ -158,7 +158,6 @@
     Context.generic -> Context.generic
   val generic_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism ->
     Context.generic -> Context.generic
-  val class_alias: binding -> class -> Proof.context -> Proof.context
   val type_alias: binding -> string -> Proof.context -> Proof.context
   val const_alias: binding -> string -> Proof.context -> Proof.context
   val fact_alias: binding -> string -> Proof.context -> Proof.context
@@ -1184,7 +1183,6 @@
 
 (* aliases *)
 
-fun class_alias b c ctxt = (map_tsig o apfst) (Type.class_alias (naming_of ctxt) b c) ctxt;
 fun type_alias b c ctxt = (map_tsig o apfst) (Type.type_alias (naming_of ctxt) b c) ctxt;
 fun const_alias b c ctxt = (map_consts o apfst) (Consts.alias (naming_of ctxt) b c) ctxt;
 fun fact_alias b c ctxt = map_facts (Facts.alias (naming_of ctxt) b c) ctxt;
diff -r 453f9cabddb5 -r da3b0e848182 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Sat Jul 01 16:39:56 2017 +0200
+++ b/src/Pure/sign.ML	Mon Jul 03 09:12:13 2017 +0200
@@ -53,7 +53,6 @@
   val intern_class: theory -> xstring -> string
   val intern_type: theory -> xstring -> string
   val intern_const: theory -> xstring -> string
-  val class_alias: binding -> class -> theory -> theory
   val type_alias: binding -> string -> theory -> theory
   val const_alias: binding -> string -> theory -> theory
   val arity_number: theory -> string -> int
@@ -246,7 +245,6 @@
 val intern_type = Name_Space.intern o type_space;
 val intern_const = Name_Space.intern o const_space;
 
-fun class_alias b c thy = map_tsig (Type.class_alias (naming_of thy) b c) thy;
 fun type_alias b c thy = map_tsig (Type.type_alias (naming_of thy) b c) thy;
 fun const_alias b c thy = map_consts (Consts.alias (naming_of thy) b c) thy;
 
diff -r 453f9cabddb5 -r da3b0e848182 src/Pure/type.ML
--- a/src/Pure/type.ML	Sat Jul 01 16:39:56 2017 +0200
+++ b/src/Pure/type.ML	Mon Jul 03 09:12:13 2017 +0200
@@ -29,7 +29,6 @@
   val change_ignore: tsig -> tsig
   val empty_tsig: tsig
   val class_space: tsig -> Name_Space.T
-  val class_alias: Name_Space.naming -> binding -> string -> tsig -> tsig
   val defaultS: tsig -> sort
   val logical_types: tsig -> string list
   val eq_sort: tsig -> sort * sort -> bool
@@ -202,9 +201,6 @@
 
 val class_space = #1 o #classes o rep_tsig;
 
-fun class_alias naming binding name = map_tsig (fn ((space, classes), default, types) =>
-  ((Name_Space.alias naming binding name space, classes), default, types));
-
 fun defaultS (TSig {default, ...}) = default;
 fun logical_types (TSig {log_types, ...}) = log_types;