--- a/src/Pure/Isar/local_theory.ML Mon Jul 03 09:12:13 2017 +0200
+++ b/src/Pure/Isar/local_theory.ML Mon Jul 03 09:20:24 2017 +0200
@@ -293,7 +293,7 @@
let val binding' = Morphism.binding phi binding in
Context.mapping
(Global_Theory.alias_fact binding' name)
- (Proof_Context.fact_alias binding' name)
+ (Proof_Context.alias_fact binding' name)
end));
--- a/src/Pure/Isar/proof_context.ML Mon Jul 03 09:12:13 2017 +0200
+++ b/src/Pure/Isar/proof_context.ML Mon Jul 03 09:20:24 2017 +0200
@@ -132,6 +132,7 @@
val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list ->
Proof.context -> (string * thm list) list * Proof.context
val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
+ val alias_fact: binding -> string -> Proof.context -> Proof.context
val read_var: binding * string option * mixfix -> Proof.context ->
(binding * typ option * mixfix) * Proof.context
val cert_var: binding * typ option * mixfix -> Proof.context ->
@@ -160,7 +161,6 @@
Context.generic -> Context.generic
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
val add_const_constraint: string * typ option -> Proof.context -> Proof.context
val add_abbrev: string -> binding * term -> Proof.context -> (term * term) * Proof.context
val revert_abbrev: string -> string -> Proof.context -> Proof.context
@@ -1088,6 +1088,8 @@
end;
+fun alias_fact b c ctxt = map_facts (Facts.alias (naming_of ctxt) b c) ctxt;
+
(** basic logical entities **)
@@ -1185,7 +1187,6 @@
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;
(* local constants *)