yet another attempt for terminology: foo_target_bar denotes an operation bar operating solely on the target context of target foo, foo_bar denotes a whole stack of operations to accomplish bar for target foo

--- a/src/Pure/Isar/class.ML	Sun Jun 08 23:30:50 2014 +0200
+++ b/src/Pure/Isar/class.ML	Sun Jun 08 23:30:51 2014 +0200
@@ -333,12 +333,12 @@
     val rhs2 = Morphism.term phi2 rhs;
   in n1 = n2 andalso Term.aconv_untyped (rhs1, rhs2) end;
 
-fun const_declaration class phi0 prmode ((b, _), rhs) =
+fun target_const class phi0 prmode ((b, _), rhs) =
   let
     val guess_identity = guess_morphism_identity (b, rhs) Morphism.identity;
     val guess_canonical = guess_morphism_identity (b, rhs) phi0;
   in
-    Generic_Target.locale_const_declaration class
+    Generic_Target.locale_target_const class
       (not o (guess_identity orf guess_canonical)) prmode ((b, NoSyn), rhs)
   end;
 
@@ -399,10 +399,10 @@
     val dangling_params = map (Morphism.term phi) (uncurry append (dangling_params_for lthy class params));
   in
     lthy
-    |> const_declaration class phi Syntax.mode_default ((b, mx), lhs)
+    |> target_const class phi Syntax.mode_default ((b, mx), lhs)
     |> Local_Theory.raw_theory (canonical_const class phi dangling_params
          ((Morphism.binding phi b, if null dangling_params then mx else NoSyn), Morphism.term phi lhs))
-    |> Generic_Target.standard_const_declaration (fn (this, other) => other <> 0 andalso this <> other)
+    |> Generic_Target.standard_const (fn (this, other) => other <> 0 andalso this <> other)
          Syntax.mode_default ((b, if null dangling_params then NoSyn else mx), lhs)
     |> synchronize_class_syntax_target class
   end;
@@ -413,10 +413,10 @@
     val dangling_term_params = map (Morphism.term phi) (snd (dangling_params_for lthy class params));
   in
     lthy
-    |> const_declaration class phi prmode ((b, mx), lhs)
+    |> target_const class phi prmode ((b, mx), lhs)
     |> Local_Theory.raw_theory (canonical_abbrev class phi prmode dangling_term_params
          ((Morphism.binding phi b, if null dangling_term_params then mx else NoSyn), rhs'))
-    |> Generic_Target.standard_const_declaration (fn (this, other) => other <> 0 andalso this <> other)
+    |> Generic_Target.standard_const (fn (this, other) => other <> 0 andalso this <> other)
          prmode ((b, if null dangling_term_params then NoSyn else mx), lhs)
     |> synchronize_class_syntax_target class
   end;

--- a/src/Pure/Isar/generic_target.ML	Sun Jun 08 23:30:50 2014 +0200
+++ b/src/Pure/Isar/generic_target.ML	Sun Jun 08 23:30:51 2014 +0200
@@ -11,7 +11,7 @@
   val standard_declaration: (int * int -> bool) -> declaration -> local_theory -> local_theory
 
   (* consts *)
-  val standard_const_declaration: (int * int -> bool) -> Syntax.mode -> (binding * mixfix) * term ->
+  val standard_const: (int * int -> bool) -> Syntax.mode -> (binding * mixfix) * term ->
     local_theory -> local_theory
 
   (* background operations *)
@@ -52,8 +52,8 @@
     (Attrib.binding * (thm list * Args.src list) list) list ->
     (Attrib.binding * (thm list * Args.src list) list) list ->
     local_theory -> local_theory
-  val locale_declaration: string -> bool -> declaration -> local_theory -> local_theory
-  val locale_const_declaration: string -> (morphism -> bool) -> Syntax.mode ->
+  val locale_target_declaration: string -> bool -> declaration -> local_theory -> local_theory
+  val locale_target_const: string -> (morphism -> bool) -> Syntax.mode ->
     (binding * mixfix) * term -> local_theory -> local_theory
   val locale_const: string -> Syntax.mode -> (binding * mixfix) * term ->
     local_theory -> local_theory
@@ -138,7 +138,7 @@
     end
   else context;
 
-fun standard_const_declaration pred prmode ((b, mx), rhs) =
+fun standard_const pred prmode ((b, mx), rhs) =
   standard_declaration pred (const_decl (K true) prmode ((b, mx), rhs));
 
 
@@ -264,7 +264,7 @@
 
 in
 
-fun notes target_notes kind facts lthy =
+fun notes notes' kind facts lthy =
   let
     val facts' = facts
       |> map (fn (a, bs) => (a, Global_Theory.burrow_fact (Global_Theory.name_multi
@@ -274,7 +274,7 @@
     val global_facts = Global_Theory.map_facts #2 facts';
   in
     lthy
-    |> target_notes kind global_facts (Attrib.partial_evaluation lthy local_facts)
+    |> notes' kind global_facts (Attrib.partial_evaluation lthy local_facts)
     |> Attrib.local_notes kind local_facts
   end;
 
@@ -283,7 +283,7 @@
 
 (* abbrev *)
 
-fun abbrev target_abbrev prmode ((b, mx), rhs) lthy =
+fun abbrev abbrev' prmode ((b, mx), rhs) lthy =
   let
     val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy);
 
@@ -298,7 +298,7 @@
     val type_params = map (Logic.mk_type o TFree) extra_tfrees;
   in
     lthy
-    |> target_abbrev prmode (b, mx') global_rhs (type_params, term_params)
+    |> abbrev' prmode (b, mx') global_rhs (type_params, term_params)
     |> Proof_Context.add_abbrev Print_Mode.internal (b, rhs) |> snd
     |> Local_Defs.fixed_abbrev ((b, NoSyn), rhs)
   end;
@@ -308,7 +308,7 @@
 
 fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
   background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params)
-  #-> (fn (lhs, def) => standard_const_declaration (op <>) Syntax.mode_default ((b, mx), lhs)
+  #-> (fn (lhs, def) => standard_const (op <>) Syntax.mode_default ((b, mx), lhs)
     #> pair (lhs, def));
 
 fun theory_notes kind global_facts local_facts =
@@ -323,7 +323,7 @@
     (Sign.add_abbrev (#1 prmode) (b, global_rhs) #->
       (fn (lhs, _) =>  (* FIXME type_params!? *)
         Sign.notation true prmode [(lhs, check_mixfix_global (b, null (snd params)) mx)] #> pair lhs))
-  #-> (fn lhs => standard_const_declaration (op <>) prmode
+  #-> (fn lhs => standard_const (op <>) prmode
           ((b, if null (snd params) then NoSyn else mx), Term.list_comb (Logic.unvarify_global lhs, snd params)));
 
 val theory_registration =
@@ -340,17 +340,17 @@
       Locale.add_thmss locale kind (standard_facts lthy ctxt local_facts))) #>
   standard_notes (fn (this, other) => other <> 0 andalso this <> other) kind local_facts;
 
-fun locale_declaration locale syntax decl lthy = lthy
+fun locale_target_declaration locale syntax decl lthy = lthy
   |> Local_Theory.target (fn ctxt => ctxt |>
     Locale.add_declaration locale syntax
       (Morphism.transform (Local_Theory.standard_morphism lthy ctxt) decl));
 
-fun locale_const_declaration locale phi_pred prmode ((b, mx), rhs) =
-  locale_declaration locale true (const_decl phi_pred prmode ((b, mx), rhs))
+fun locale_target_const locale phi_pred prmode ((b, mx), rhs) =
+  locale_target_declaration locale true (const_decl phi_pred prmode ((b, mx), rhs))
 
 fun locale_const locale prmode ((b, mx), rhs) =
-  locale_const_declaration locale (K true) prmode ((b, mx), rhs)
-  #> standard_const_declaration (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, mx), rhs);
+  locale_target_const locale (K true) prmode ((b, mx), rhs)
+  #> standard_const (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, mx), rhs);
 
 fun locale_dependency locale dep_morph mixin export =
   (Local_Theory.raw_theory ooo Locale.add_dependency locale) dep_morph mixin export

--- a/src/Pure/Isar/named_target.ML	Sun Jun 08 23:30:50 2014 +0200
+++ b/src/Pure/Isar/named_target.ML	Sun Jun 08 23:30:51 2014 +0200
@@ -105,7 +105,7 @@
 fun declaration (Target {target, is_locale, ...}) {syntax, pervasive} decl =
   if is_locale then
     pervasive ? Generic_Target.background_declaration decl
-    #> Generic_Target.locale_declaration target syntax decl
+    #> Generic_Target.locale_target_declaration target syntax decl
     #> Generic_Target.standard_declaration (fn (_, other) => other <> 0) decl
   else Generic_Target.theory_declaration decl;