# HG changeset patch
# User wenzelm
# Date 1407692660 -7200
# Node ID 44354c99d75405b19d1366bcfc89813d9ac0a989
# Parent  7cae177c9084afcbaf2cd1e7c6e61ca2c1c077f1
support aliases within the facts space;

diff -r 7cae177c9084 -r 44354c99d754 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Aug 10 16:13:12 2014 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sun Aug 10 19:44:20 2014 +0200
@@ -154,6 +154,7 @@
   val class_alias: binding -> class -> Proof.context -> Proof.context
   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
@@ -1084,6 +1085,7 @@
 fun class_alias b c ctxt = (map_tsig o apfst) (Type.class_alias (naming_of ctxt) b c) ctxt;
 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 *)
diff -r 7cae177c9084 -r 44354c99d754 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 *)
diff -r 7cae177c9084 -r 44354c99d754 src/Pure/global_theory.ML
--- 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);