# HG changeset patch
# User wenzelm
# Date 1139776466 -3600
# Node ID d25dfb7976127f59b95f72f42ff87045ddd8da33
# Parent  0059b5b195a21d7a15b3f02969482de2af3615a6
tuned;

diff -r 0059b5b195a2 -r d25dfb797612 NEWS
--- a/NEWS	Sun Feb 12 21:34:25 2006 +0100
+++ b/NEWS	Sun Feb 12 21:34:26 2006 +0100
@@ -357,10 +357,14 @@
 Note that fold_index starts counting at index 0, not 1 like foldln
 used to.
 
-* Pure/General: name_mangler.ML provides a functor for generic name
+* Pure/General/name_mangler.ML provides a functor for generic name
 mangling (bijective mapping from any expression values to strings).
 
-* Pure/General: rat.ML implements rational numbers.
+* Pure/General/rat.ML implements rational numbers.
+
+* Pure/General/table.ML: the join operations now works via exceptions
+DUP/SAME instead of type option.  This is simpler in simple cases, and
+admits slightly more efficient complex applications.
 
 * Pure: datatype Context.generic joins theory/Proof.context and
 provides some facilities for code that works in either kind of
diff -r 0059b5b195a2 -r d25dfb797612 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Sun Feb 12 21:34:25 2006 +0100
+++ b/src/Pure/Isar/local_theory.ML	Sun Feb 12 21:34:26 2006 +0100
@@ -100,14 +100,11 @@
 
 (* theory/locale substructures *)
 
-fun transfer thy =
-  ProofContext.transfer thy #> map_locale (ProofContext.transfer thy);
-
-fun theory f ctxt = transfer (f (ProofContext.theory_of ctxt)) ctxt;
-
 fun theory_result f ctxt =
   let val (res, thy') = f (ProofContext.theory_of ctxt)
-  in (res, transfer thy' ctxt) end;
+  in (res, ctxt |> map_locale (ProofContext.transfer thy') |> ProofContext.transfer thy') end;
+
+fun theory f ctxt = #2 (theory_result (f #> pair ()) ctxt);
 
 fun locale_result f ctxt =
   (case locale_of ctxt of
@@ -116,7 +113,7 @@
       let
         val (res, loc_ctxt') = f view_ctxt;
         val thy' = ProofContext.theory_of loc_ctxt';
-      in (res, ctxt |> map_locale (K loc_ctxt') |> transfer thy') end);
+      in (res, ctxt |> map_locale (K loc_ctxt') |> ProofContext.transfer thy') end);
 
 fun locale f ctxt =
   if is_none (locale_of ctxt) then ctxt