--- 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;