# HG changeset patch
# User haftmann
# Date 1548004549 0
# Node ID 82f57315cadeabf25ef8f934d6c3ee7d9ae886b2
# Parent  1a249d1c884b1cefb0cfdef74d36c4af27405288
dedicated combinator for declarations nested in a local theory block

diff -r 1a249d1c884b -r 82f57315cade src/Pure/Isar/interpretation.ML
--- a/src/Pure/Isar/interpretation.ML	Sun Jan 20 17:15:47 2019 +0000
+++ b/src/Pure/Isar/interpretation.ML	Sun Jan 20 17:15:49 2019 +0000
@@ -55,23 +55,14 @@
     val lthy' = Variable.declare_term rhs lthy;
     val ((_, (_, def)), lthy'') =
       Local_Theory.define ((b, mx), ((Thm.def_binding_optional b name, atts), rhs)) lthy';
-  in (def, lthy'') end;
+  in (Thm.symmetric def, lthy'') end;
 
-fun augment_with_defs _ [] _ ctxt = ([], ctxt)
+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 lthy =
-      let
-        val (_, inner_lthy) =
-          Local_Theory.open_target lthy
-          ||> fold Locale.activate_declarations deps;
-        val (inner_defs, inner_lthy') =
-          fold_map (augment_with_def prep_term) raw_defs inner_lthy;
-        val lthy' =
-          inner_lthy'
-          |> Local_Theory.close_target;
-        val def_eqns =
-          map (singleton (Proof_Context.export inner_lthy' lthy') o Thm.symmetric) inner_defs
-      in (def_eqns, lthy') end;
+  | 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);
 
 fun prep_interpretation prep_expr prep_term
   expression raw_defs initial_ctxt =
diff -r 1a249d1c884b -r 82f57315cade src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Sun Jan 20 17:15:47 2019 +0000
+++ b/src/Pure/Isar/local_theory.ML	Sun Jan 20 17:15:49 2019 +0000
@@ -78,6 +78,9 @@
     operations -> local_theory -> Binding.scope * local_theory
   val open_target: local_theory -> Binding.scope * local_theory
   val close_target: local_theory -> 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;
 
 structure Local_Theory: LOCAL_THEORY =
@@ -395,4 +398,23 @@
     val ({after_close, ...} :: rest) = Data.get lthy;
   in lthy |> Data.put rest |> reset |> after_close end;
 
+fun subtarget g lthy =
+  lthy
+  |> open_target
+  |> snd
+  |> g
+  |> close_target;
+
+fun subtarget_result f g lthy =
+  let
+    val (x, inner_lthy) =
+      open_target lthy
+      |> snd
+      |> g
+    val lthy' =
+      inner_lthy
+      |> close_target;
+    val phi = Proof_Context.export_morphism inner_lthy lthy'
+  in (f phi x, lthy') end;
+
 end;