src/Pure/global_theory.ML

 sig
   val facts_of: theory -> Facts.T
   val check_fact: theory -> xstring * Position.T -> string
   val intern_fact: theory -> xstring -> string
   val defined_fact: theory -> string -> bool
+  val alias_fact: binding -> string -> theory -> theory
   val hide_fact: bool -> string -> theory -> theory
   val get_thms: theory -> xstring -> thm list
   val get_thm: theory -> xstring -> thm
   val all_thms_of: theory -> bool -> (string * thm) list
   val map_facts: ('a -> 'b) -> ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list

 
 fun check_fact thy = Facts.check (Context.Theory thy) (facts_of thy);
 val intern_fact = Facts.intern o facts_of;
 val defined_fact = Facts.defined o facts_of;
 
+fun alias_fact binding name thy =
+  Data.map (Facts.alias (Sign.naming_of thy) binding name) thy;
+
 fun hide_fact fully name = Data.map (Facts.hide fully name);
 
 
 (* retrieve theorems *)