--- 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
--- 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