# HG changeset patch
# User haftmann
# Date 1366738833 -7200
# Node ID 789507cd689ded3f63e662abd20f136a42a75428
# Parent  e4b5bebe5235c545866266c635746d110f67028f
dropped dead code

diff -r e4b5bebe5235 -r 789507cd689d src/Pure/Isar/expression.ML
--- 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;