# HG changeset patch
# User haftmann
# Date 1602487538 0
# Node ID e51f1733618d36b8a3628c1134a3ac4bba0ba9cc
# Parent  24bd1316eaae0806c4324a397bbfa6297726858f
replaced combinators by more conventional nesting pattern

diff -r 24bd1316eaae -r e51f1733618d NEWS
--- a/NEWS	Mon Oct 12 07:25:38 2020 +0000
+++ b/NEWS	Mon Oct 12 07:25:38 2020 +0000
@@ -61,6 +61,10 @@
 
   * Local_Theory.end_nested replaces Local_Theory.close_target.
 
+  * Combination of Local_Theory.begin_nested and
+    Local_Theory.end_nested(_result) replaces
+    Local_Theory.subtarget(_result).
+
 INCOMPATIBILITY.
 
 
diff -r 24bd1316eaae -r e51f1733618d src/Pure/Isar/interpretation.ML
--- a/src/Pure/Isar/interpretation.ML	Mon Oct 12 07:25:38 2020 +0000
+++ b/src/Pure/Isar/interpretation.ML	Mon Oct 12 07:25:38 2020 +0000
@@ -60,9 +60,11 @@
 fun augment_with_defs _ [] _ = pair []
       (*quasi-inhomogeneous type: definitions demand local theory rather than bare proof context*)
   | augment_with_defs prep_term raw_defs deps =
-      Local_Theory.subtarget_result Morphism.fact
-        (fold Locale.activate_declarations deps
-         #> fold_map (augment_with_def prep_term) raw_defs);
+      Local_Theory.begin_nested
+      #> snd
+      #> fold Locale.activate_declarations deps
+      #> fold_map (augment_with_def prep_term) raw_defs
+      #> Local_Theory.end_nested_result Morphism.fact;
 
 fun prep_interpretation prep_expr prep_term
   expression raw_defs initial_ctxt =
diff -r 24bd1316eaae -r e51f1733618d src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Mon Oct 12 07:25:38 2020 +0000
+++ b/src/Pure/Isar/local_theory.ML	Mon Oct 12 07:25:38 2020 +0000
@@ -76,9 +76,6 @@
   val begin_nested: local_theory -> Binding.scope * local_theory
   val end_nested: local_theory -> local_theory
   val end_nested_result: (morphism -> 'a -> 'b) ->  'a * local_theory -> 'b * local_theory
-  val subtarget: (local_theory -> local_theory) -> local_theory -> local_theory
-  val subtarget_result: (morphism -> 'a -> 'b) -> (local_theory -> 'a * local_theory) ->
-    local_theory -> 'b * local_theory
 end;
 
 signature PRIVATE_LOCAL_THEORY =
@@ -404,13 +401,4 @@
     val phi = Proof_Context.export_morphism lthy outer_lthy;
   in (decl phi x, outer_lthy) end;
 
-fun subtarget body = begin_nested #> snd #> body #> end_nested;
-
-fun subtarget_result decl body lthy =
-  let
-    val (x, inner_lthy) = lthy |> begin_nested |> snd |> body;
-    val lthy' = inner_lthy |> end_nested;
-    val phi = Proof_Context.export_morphism inner_lthy lthy';
-  in (decl phi x, lthy') end;
-
 end;