more general standard_declaration;
generic const declaration, which is applied to nested targets (named target only);

--- a/src/Pure/Isar/generic_target.ML	Mon Apr 02 23:27:24 2012 +0200
+++ b/src/Pure/Isar/generic_target.ML	Mon Apr 02 23:55:25 2012 +0200
@@ -25,7 +25,11 @@
     string * bool -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory
   val background_declaration: declaration -> local_theory -> local_theory
   val locale_declaration: string -> bool -> declaration -> local_theory -> local_theory
-  val standard_declaration: declaration -> local_theory -> local_theory
+  val standard_declaration: (int -> bool) -> declaration -> local_theory -> local_theory
+  val generic_const: bool -> Syntax.mode -> (binding * mixfix) * term ->
+    Context.generic -> Context.generic
+  val const_declaration: (int -> bool) -> Syntax.mode -> (binding * mixfix) * term ->
+    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 ->
@@ -215,9 +219,55 @@
     Locale.add_declaration locale syntax
       (Morphism.transform (Local_Theory.standard_morphism lthy ctxt) decl));
 
-fun standard_declaration decl lthy =
-  Local_Theory.map_contexts (fn _ => fn ctxt =>
-    Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt) lthy;
+fun standard_declaration pred decl lthy =
+  Local_Theory.map_contexts (fn level => fn ctxt =>
+    if pred level then Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt
+    else ctxt) lthy;
+
+
+(* const declaration *)
+
+fun generic_const same_shape prmode ((b, mx), t) context =
+  let
+    val const_alias =
+      if same_shape then
+        (case t of
+          Const (c, T) =>
+            let
+              val thy = Context.theory_of context;
+              val ctxt = Context.proof_of context;
+              val t' = Syntax.check_term ctxt (Const (c, dummyT))
+                |> singleton (Variable.polymorphic ctxt);
+            in
+              (case t' of
+                Const (c', T') =>
+                  if c = c' andalso Sign.typ_equiv thy (T, T') then SOME c else NONE
+              | _ => NONE)
+            end
+        | _ => NONE)
+      else NONE;
+  in
+    (case const_alias of
+      SOME c =>
+        context
+        |> Context.mapping (Sign.const_alias b c) (Proof_Context.const_alias b c)
+        |> Morphism.form (Proof_Context.generic_notation true prmode [(t, mx)])
+    | NONE =>
+        context
+        |> Proof_Context.generic_add_abbrev Print_Mode.internal (b, t)
+        |-> (fn (const as Const (c, _), _) => same_shape ?
+              (Proof_Context.generic_revert_abbrev (#1 prmode) c #>
+               Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)]))))
+  end;
+
+fun const_declaration pred prmode ((b, mx), rhs) =
+  standard_declaration pred (fn phi =>
+    let
+      val b' = Morphism.binding phi b;
+      val rhs' = Morphism.term phi rhs;
+      val rhs'' = Term.close_schematic_term rhs';
+      val same_shape = Term.aconv_untyped (rhs, rhs');
+    in generic_const same_shape prmode ((b', mx), rhs'') end);
 
 
 
@@ -248,6 +298,6 @@
       (fn (lhs, _) => Sign.notation true prmode [(lhs, mx)]));
 
 fun theory_declaration decl =
-  background_declaration decl #> standard_declaration decl;
+  background_declaration decl #> standard_declaration (K true) decl;
 
 end;

--- a/src/Pure/Isar/named_target.ML	Mon Apr 02 23:27:24 2012 +0200
+++ b/src/Pure/Isar/named_target.ML	Mon Apr 02 23:55:25 2012 +0200
@@ -46,40 +46,7 @@
 
 (* consts in locale *)
 
-fun generic_const same_shape prmode ((b, mx), t) context =
-  let
-    val const_alias =
-      if same_shape then
-        (case t of
-          Const (c, T) =>
-            let
-              val thy = Context.theory_of context;
-              val ctxt = Context.proof_of context;
-              val t' = Syntax.check_term ctxt (Const (c, dummyT))
-                |> singleton (Variable.polymorphic ctxt);
-            in
-              (case t' of
-                Const (c', T') =>
-                  if c = c' andalso Sign.typ_equiv thy (T, T') then SOME c else NONE
-              | _ => NONE)
-            end
-        | _ => NONE)
-      else NONE;
-  in
-    (case const_alias of
-      SOME c =>
-        context
-        |> Context.mapping (Sign.const_alias b c) (Proof_Context.const_alias b c)
-        |> Morphism.form (Proof_Context.generic_notation true prmode [(t, mx)])
-    | NONE =>
-        context
-        |> Proof_Context.generic_add_abbrev Print_Mode.internal (b, t)
-        |-> (fn (const as Const (c, _), _) => same_shape ?
-              (Proof_Context.generic_revert_abbrev (#1 prmode) c #>
-               Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)]))))
-  end;
-
-fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) =
+fun locale_const (Target {target, is_class, ...}) prmode ((b, mx), rhs) =
   Generic_Target.locale_declaration target true (fn phi =>
     let
       val b' = Morphism.binding phi b;
@@ -94,27 +61,36 @@
           andalso not (null prefix')
           andalso List.last prefix' = (Class.class_prefix target, false)
         orelse same_shape);
-    in not is_canonical_class ? generic_const same_shape prmode ((b', mx), rhs'') end);
+    in
+      not is_canonical_class ? Generic_Target.generic_const same_shape prmode ((b', mx), rhs'')
+    end) #>
+  (fn lthy => lthy |> Generic_Target.const_declaration
+    (fn level => level <> 0 andalso level <> Local_Theory.level lthy) prmode ((b, mx), rhs));
 
 
 (* define *)
 
+fun global_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
+  Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params)
+  #-> (fn (lhs, def) => Generic_Target.const_declaration (K true) Syntax.mode_default ((b, mx), lhs)
+    #> pair (lhs, def));
+
 fun locale_foundation ta (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
   Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
   #-> (fn (lhs, def) => locale_const ta Syntax.mode_default ((b, mx), lhs)
-    #> pair (lhs, def))
+    #> pair (lhs, def));
 
 fun class_foundation (ta as Target {target, ...})
     (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
   Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
   #-> (fn (lhs, def) => locale_const ta Syntax.mode_default ((b, NoSyn), lhs)
     #> Class.const target ((b, mx), (type_params, lhs))
-    #> pair (lhs, def))
+    #> pair (lhs, def));
 
 fun target_foundation (ta as Target {is_locale, is_class, ...}) =
   if is_class then class_foundation ta
   else if is_locale then locale_foundation ta
-  else Generic_Target.theory_foundation;
+  else global_foundation;
 
 
 (* notes *)
@@ -151,9 +127,7 @@
     lthy
     |> pervasive ? Generic_Target.background_declaration decl
     |> Generic_Target.locale_declaration target syntax decl
-    |> (fn lthy' => lthy' |> Local_Theory.map_contexts (fn level => fn ctxt =>
-        if level = 0 then ctxt
-        else Context.proof_map (Local_Theory.standard_form lthy' ctxt decl) ctxt));
+    |> (fn lthy' => lthy' |> Generic_Target.standard_declaration (fn level => level <> 0) decl);
 
 
 (* pretty *)