--- a/src/Pure/Isar/expression.ML Tue Apr 23 19:31:24 2013 +0200
+++ b/src/Pure/Isar/expression.ML Tue Apr 23 19:40:33 2013 +0200
@@ -858,7 +858,6 @@
val activate_proof = Context.proof_map ooo Locale.add_registration;
val activate_local_theory = Local_Theory.target ooo activate_proof;
val add_registration = Local_Theory.raw_theory o Context.theory_map ooo Locale.add_registration;
-val add_registration_global = Proof_Context.background_theory o Context.theory_map ooo Locale.add_registration;
fun add_dependency locale = Local_Theory.raw_theory ooo Locale.add_dependency locale;
fun add_dependency_global locale = Proof_Context.background_theory ooo Locale.add_dependency locale;