--- a/src/Pure/Isar/local_theory.ML Wed Oct 28 00:24:38 2009 +0100
+++ b/src/Pure/Isar/local_theory.ML Wed Oct 28 16:25:10 2009 +0100
@@ -15,6 +15,7 @@
val map_naming: (Name_Space.naming -> Name_Space.naming) -> local_theory -> local_theory
val conceal: local_theory -> local_theory
val set_group: serial -> local_theory -> local_theory
+ val restore_naming: local_theory -> local_theory -> local_theory
val target_of: local_theory -> Proof.context
val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
val raw_theory: (theory -> theory) -> local_theory -> local_theory
@@ -111,6 +112,8 @@
val conceal = map_naming Name_Space.conceal;
val set_group = map_naming o Name_Space.set_group;
+val restore_naming = map_naming o K o naming_of;
+
(* target *)