# HG changeset patch
# User wenzelm
# Date 1256743510 -3600
# Node ID f2bc8bc6e73d8ca779de7d81d8e7537cb18168e3
# Parent  02de0317f66fb7509c0e48b5c99f4175a3ed9df6
added restore_naming;

diff -r 02de0317f66f -r f2bc8bc6e73d src/Pure/Isar/local_theory.ML
--- 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 *)