allow "pervasive" local theory declarations, which are applied the background theory;

--- a/src/Pure/Isar/isar_cmd.ML	Thu Nov 05 20:44:42 2009 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Thu Nov 05 22:06:46 2009 +0100
@@ -16,7 +16,7 @@
   val oracle: bstring * Position.T -> Symbol_Pos.text * Position.T -> theory -> theory
   val add_axioms: ((binding * string) * Attrib.src list) list -> theory -> theory
   val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory
-  val declaration: Symbol_Pos.text * Position.T -> local_theory -> local_theory
+  val declaration: bool -> Symbol_Pos.text * Position.T -> local_theory -> local_theory
   val simproc_setup: string -> string list -> Symbol_Pos.text * Position.T -> string list ->
     local_theory -> local_theory
   val hide_names: bool -> string * xstring list -> theory -> theory
@@ -178,10 +178,10 @@
 
 (* declarations *)
 
-fun declaration (txt, pos) =
+fun declaration pervasive (txt, pos) =
   txt |> ML_Context.expression pos
     "val declaration: Morphism.declaration"
-    "Context.map_proof (LocalTheory.declaration declaration)"
+    ("Context.map_proof (LocalTheory.declaration " ^ Bool.toString pervasive ^ " declaration)")
   |> Context.proof_map;
 
 

--- a/src/Pure/Isar/isar_syn.ML	Thu Nov 05 20:44:42 2009 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Thu Nov 05 22:06:46 2009 +0100
@@ -22,8 +22,9 @@
   "advanced", "and", "assumes", "attach", "begin", "binder",
   "constrains", "defines", "fixes", "for", "identifier", "if",
   "imports", "in", "infix", "infixl", "infixr", "is",
-  "notes", "obtains", "open", "output", "overloaded", "shows",
-  "structure", "unchecked", "uses", "where", "|"];
+  "notes", "obtains", "open", "output", "overloaded", "pervasive",
+  "shows", "structure", "unchecked", "uses", "where", "|"];
+
 
 
 (** init and exit **)
@@ -337,7 +338,7 @@
 
 val _ =
   OuterSyntax.local_theory "declaration" "generic ML declaration" (K.tag_ml K.thy_decl)
-    (P.ML_source >> IsarCmd.declaration);
+    (P.opt_keyword "pervasive" -- P.ML_source >> uncurry IsarCmd.declaration);
 
 val _ =
   OuterSyntax.local_theory "simproc_setup" "define simproc in ML" (K.tag_ml K.thy_decl)

--- a/src/Pure/Isar/local_theory.ML	Thu Nov 05 20:44:42 2009 +0100
+++ b/src/Pure/Isar/local_theory.ML	Thu Nov 05 22:06:46 2009 +0100
@@ -27,6 +27,7 @@
   val map_contexts: (Context.generic -> Context.generic) -> local_theory -> local_theory
   val standard_morphism: local_theory -> Proof.context -> morphism
   val target_morphism: local_theory -> morphism
+  val global_morphism: local_theory -> morphism
   val pretty: local_theory -> Pretty.T list
   val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory
@@ -35,9 +36,9 @@
   val note: string -> Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory
   val notes: string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
     local_theory -> (string * thm list) list * local_theory
-  val type_syntax: declaration -> local_theory -> local_theory
-  val term_syntax: declaration -> local_theory -> local_theory
-  val declaration: declaration -> local_theory -> local_theory
+  val type_syntax: bool -> declaration -> local_theory -> local_theory
+  val term_syntax: bool -> declaration -> local_theory -> local_theory
+  val declaration: bool -> declaration -> local_theory -> local_theory
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
   val init: string -> operations -> Proof.context -> local_theory
   val restore: local_theory -> local_theory
@@ -65,9 +66,9 @@
   notes: string ->
     (Attrib.binding * (thm list * Attrib.src list) list) list ->
     local_theory -> (string * thm list) list * local_theory,
-  type_syntax: declaration -> local_theory -> local_theory,
-  term_syntax: declaration -> local_theory -> local_theory,
-  declaration: declaration -> local_theory -> local_theory,
+  type_syntax: bool -> declaration -> local_theory -> local_theory,
+  term_syntax: bool -> declaration -> local_theory -> local_theory,
+  declaration: bool -> declaration -> local_theory -> local_theory,
   reinit: local_theory -> local_theory,
   exit: local_theory -> Proof.context};
 
@@ -174,27 +175,27 @@
   Morphism.binding_morphism (Name_Space.transform_binding (naming_of lthy));
 
 fun target_morphism lthy = standard_morphism lthy (target_of lthy);
+fun global_morphism lthy = standard_morphism lthy (ProofContext.init (ProofContext.theory_of lthy));
 
 
 (* basic operations *)
 
 fun operation f lthy = f (#operations (get_lthy lthy)) lthy;
-fun operation1 f x = operation (fn ops => f ops x);
 fun operation2 f x y lthy = operation (fn ops => f ops x y) lthy;
 
 val pretty = operation #pretty;
 val abbrev = apsnd checkpoint ooo operation2 #abbrev;
 val define = apsnd checkpoint ooo operation2 #define;
 val notes = apsnd checkpoint ooo operation2 #notes;
-val type_syntax = checkpoint oo operation1 #type_syntax;
-val term_syntax = checkpoint oo operation1 #term_syntax;
-val declaration = checkpoint oo operation1 #declaration;
+val type_syntax = checkpoint ooo operation2 #type_syntax;
+val term_syntax = checkpoint ooo operation2 #term_syntax;
+val declaration = checkpoint ooo operation2 #declaration;
 
 fun note kind (a, ths) = notes kind [(a, [(ths, [])])] #>> the_single;
 
 fun notation add mode raw_args lthy =
   let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args
-  in term_syntax (ProofContext.target_notation add mode args) lthy end;
+  in term_syntax false (ProofContext.target_notation add mode args) lthy end;
 
 
 (* init *)

--- a/src/Pure/Isar/theory_target.ML	Thu Nov 05 20:44:42 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML	Thu Nov 05 22:06:46 2009 +0100
@@ -71,26 +71,38 @@
      else pretty_thy ctxt target is_class);
 
 
-(* target declarations *)
+(* generic declarations *)
+
+local
 
-fun target_decl add (Target {target, ...}) d lthy =
+fun direct_decl decl =
+  let val decl0 = Morphism.form decl in
+    LocalTheory.theory (Context.theory_map decl0) #>
+    LocalTheory.target (Context.proof_map decl0)
+  end;
+
+fun target_decl add (Target {target, ...}) pervasive decl lthy =
   let
-    val d' = Morphism.transform (LocalTheory.target_morphism lthy) d;
-    val d0 = Morphism.form d';
+    val global_decl = Morphism.transform (LocalTheory.global_morphism lthy) decl;
+    val target_decl = Morphism.transform (LocalTheory.target_morphism lthy) decl;
   in
     if target = "" then
       lthy
-      |> LocalTheory.theory (Context.theory_map d0)
-      |> LocalTheory.target (Context.proof_map d0)
+      |> direct_decl target_decl
     else
       lthy
-      |> LocalTheory.target (add target d')
+      |> pervasive ? direct_decl global_decl
+      |> LocalTheory.target (add target target_decl)
   end;
 
+in
+
 val type_syntax = target_decl Locale.add_type_syntax;
 val term_syntax = target_decl Locale.add_term_syntax;
 val declaration = target_decl Locale.add_declaration;
 
+end;
+
 fun class_target (Target {target, ...}) f =
   LocalTheory.raw_theory f #>
   LocalTheory.target (Class_Target.refresh_syntax target);
@@ -219,7 +231,7 @@
     val t = Term.list_comb (const, map Free xs);
   in
     lthy'
-    |> is_locale ? term_syntax ta (locale_const ta Syntax.mode_default ((b, mx2), t))
+    |> is_locale ? term_syntax ta false (locale_const ta Syntax.mode_default ((b, mx2), t))
     |> is_class ? class_target ta (Class_Target.declare target ((b, mx1), t))
     |> LocalDefs.add_def ((b, NoSyn), t)
   end;
@@ -244,7 +256,7 @@
         LocalTheory.theory_result (Sign.add_abbrev PrintMode.internal (b, global_rhs))
         #-> (fn (lhs, _) =>
           let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
-            term_syntax ta (locale_const ta prmode ((b, mx2), lhs')) #>
+            term_syntax ta false (locale_const ta prmode ((b, mx2), lhs')) #>
             is_class ? class_target ta (Class_Target.abbrev target prmode ((b, mx1), t'))
           end)
       else