# HG changeset patch
# User wenzelm
# Date 1332427309 -3600
# Node ID 5e70b457b704ee296cbbdf85ccfd111a744dad61
# Parent  bfad2f674d0ea3b379a8292f7902f9a277cf4871
uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
uniform treatment of target contexts as invisible;
added Local_Theory.standard_form convenience;

diff -r bfad2f674d0e -r 5e70b457b704 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Thu Mar 22 11:11:51 2012 +0100
+++ b/src/Pure/Isar/class.ML	Thu Mar 22 15:41:49 2012 +0100
@@ -557,7 +557,7 @@
         abbrev = Generic_Target.abbrev
           (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
             Generic_Target.theory_abbrev prmode ((b, mx), t)),
-        declaration = K Generic_Target.theory_declaration,
+        declaration = K Generic_Target.standard_declaration,
         pretty = pretty,
         exit = Local_Theory.target_of o conclude}
   end;
diff -r bfad2f674d0e -r 5e70b457b704 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Thu Mar 22 11:11:51 2012 +0100
+++ b/src/Pure/Isar/generic_target.ML	Thu Mar 22 15:41:49 2012 +0100
@@ -20,7 +20,9 @@
     string * bool -> (binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory
 
-  val theory_declaration: declaration -> local_theory -> local_theory
+  val background_declaration: declaration -> local_theory -> local_theory
+  val standard_declaration: declaration -> local_theory -> local_theory
+
   val theory_foundation: ((binding * typ) * mixfix) * (binding * term) ->
     term list * term list -> local_theory -> (term * thm) * local_theory
   val theory_notes: string -> (Attrib.binding * (thm list * Args.src list) list) list ->
@@ -179,20 +181,24 @@
   end;
 
 
+(* declaration *)
+
+fun background_declaration decl lthy =
+  let
+    val theory_decl =
+      Local_Theory.standard_form lthy
+        (Proof_Context.init_global (Proof_Context.theory_of lthy)) decl;
+  in Local_Theory.background_theory (Context.theory_map theory_decl) lthy end;
+
+fun standard_declaration decl =
+  background_declaration decl #>
+  (fn lthy => Local_Theory.map_contexts (fn ctxt =>
+    Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt) lthy);
+
+
 
 (** primitive theory operations **)
 
-fun theory_declaration decl lthy =
-  let
-    val global_decl = Morphism.form
-      (Morphism.transform (Local_Theory.global_morphism lthy) decl);
-  in
-    lthy
-    |> Local_Theory.background_theory (Context.theory_map global_decl)
-    |> Local_Theory.target (Context.proof_map global_decl)
-    |> Context.proof_map (Morphism.form decl)
-  end;
-
 fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
   let
     val (const, lthy2) = lthy
diff -r bfad2f674d0e -r 5e70b457b704 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Thu Mar 22 11:11:51 2012 +0100
+++ b/src/Pure/Isar/local_theory.ML	Thu Mar 22 15:41:49 2012 +0100
@@ -33,7 +33,7 @@
   val propagate_ml_env: generic_theory -> generic_theory
   val standard_morphism: local_theory -> Proof.context -> morphism
   val target_morphism: local_theory -> morphism
-  val global_morphism: local_theory -> morphism
+  val standard_form: local_theory -> Proof.context -> (morphism -> 'a) -> 'a
   val operations_of: local_theory -> operations
   val define: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory
@@ -99,7 +99,12 @@
 );
 
 fun map_contexts f =
-  (Data.map o map) (fn {naming, operations, target} => make_lthy (naming, operations, f target))
+  (Data.map o map) (fn {naming, operations, target} =>
+    make_lthy (naming, operations,
+      target
+      |> Context_Position.set_visible false
+      |> f
+      |> Context_Position.restore_visible target))
   #> f;
 
 fun assert lthy =
@@ -178,10 +183,11 @@
 
 fun target_result f lthy =
   let
-    val (res, ctxt') = target_of lthy
+    val target = target_of lthy;
+    val (res, ctxt') = target
       |> Context_Position.set_visible false
       |> f
-      ||> Context_Position.restore_visible lthy;
+      ||> Context_Position.restore_visible target;
     val thy' = Proof_Context.theory_of ctxt';
     val lthy' = lthy
       |> map_target (K ctxt')
@@ -208,8 +214,8 @@
 
 fun target_morphism lthy = standard_morphism lthy (target_of lthy);
 
-fun global_morphism lthy =
-  standard_morphism lthy (Proof_Context.init_global (Proof_Context.theory_of lthy));
+fun standard_form lthy ctxt x =
+  Morphism.form (Morphism.transform (standard_morphism lthy ctxt) x);
 
 
 
diff -r bfad2f674d0e -r 5e70b457b704 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Thu Mar 22 11:11:51 2012 +0100
+++ b/src/Pure/Isar/named_target.ML	Thu Mar 22 15:41:49 2012 +0100
@@ -61,12 +61,10 @@
   end;
 
 fun target_declaration (Target {target, ...}) {syntax, pervasive} decl lthy =
-  if target = "" then Generic_Target.theory_declaration decl lthy
+  if target = "" then Generic_Target.standard_declaration decl lthy
   else
     lthy
-    |> pervasive ? Local_Theory.background_theory
-        (Context.theory_map
-          (Morphism.form (Morphism.transform (Local_Theory.global_morphism lthy) decl)))
+    |> pervasive ? Generic_Target.background_declaration decl
     |> locale_declaration target syntax decl
     |> Context.proof_map (Morphism.form decl);
 
diff -r bfad2f674d0e -r 5e70b457b704 src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Thu Mar 22 11:11:51 2012 +0100
+++ b/src/Pure/Isar/overloading.ML	Thu Mar 22 15:41:49 2012 +0100
@@ -208,7 +208,7 @@
         abbrev = Generic_Target.abbrev
           (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
             Generic_Target.theory_abbrev prmode ((b, mx), t)),
-        declaration = K Generic_Target.theory_declaration,
+        declaration = K Generic_Target.standard_declaration,
         pretty = pretty,
         exit = Local_Theory.target_of o conclude}
   end;