src/Pure/facts.ML

--- a/src/Pure/facts.ML	Sun Aug 10 16:13:12 2014 +0200
+++ b/src/Pure/facts.ML	Sun Aug 10 19:44:20 2014 +0200
@@ -22,6 +22,7 @@
   type T
   val empty: T
   val space_of: T -> Name_Space.T
+  val alias: Name_Space.naming -> binding -> string -> T -> T
   val is_concealed: T -> string -> bool
   val check: Context.generic -> T -> xstring * Position.T -> string
   val intern: T -> xstring -> string
@@ -143,6 +144,9 @@
 
 val space_of = Name_Space.space_of_table o facts_of;
 
+fun alias naming binding name (Facts {facts, props}) =
+  make_facts (Name_Space.alias_table naming binding name facts) props;
+
 val is_concealed = Name_Space.is_concealed o space_of;
 
 fun check context facts (xname, pos) =
@@ -156,7 +160,7 @@
 
 val intern = Name_Space.intern o space_of;
 fun extern ctxt = Name_Space.extern ctxt o space_of;
-fun markup_extern ctxt = Name_Space.markup_extern ctxt o space_of
+fun markup_extern ctxt = Name_Space.markup_extern ctxt o space_of;
 
 
 (* retrieve *)