# HG changeset patch
# User wenzelm
# Date 1499066424 -7200
# Node ID c2c18b6b48daff696c2282e73165318de6987647
# Parent  da3b0e848182d05c7dfd5be6ab16fdc8240caec0
tuned signature;

diff -r da3b0e848182 -r c2c18b6b48da src/Pure/Isar/local_theory.ML
--- 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));
 
 
diff -r da3b0e848182 -r c2c18b6b48da src/Pure/Isar/proof_context.ML
--- 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 *)