--- a/src/Pure/global_theory.ML Sun Aug 10 16:13:12 2014 +0200
+++ b/src/Pure/global_theory.ML Sun Aug 10 19:44:20 2014 +0200
@@ -10,6 +10,7 @@
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
@@ -60,6 +61,9 @@
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);