src/Pure/Isar/generic_target.ML

     (string * thm list) list * local_theory
   val abbrev: (Syntax.mode -> binding * mixfix -> term ->
       term list * term list -> local_theory -> local_theory) ->
     Syntax.mode -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory
 
-  (*theory operations*)
-  val theory_foundation: ((binding * typ) * mixfix) * (binding * term) ->
-    term list * term list -> local_theory -> (term * thm) * local_theory
-  val theory_notes: string ->
+  (*theory target primitives*)
+  val theory_target_foundation: ((binding * typ) * mixfix) * (binding * term) ->
+     term list * term list -> local_theory -> (term * thm) * local_theory
+  val theory_target_notes: string ->
     (Attrib.binding * (thm list * Token.src list) list) list ->
     (Attrib.binding * (thm list * Token.src list) list) list ->
     local_theory -> local_theory
+  val theory_target_abbrev: Syntax.mode -> (binding * mixfix) -> term -> term list * term list ->
+    local_theory -> local_theory
+
+  (*theory target operations*)
   val theory_declaration: declaration -> local_theory -> local_theory
-  val theory_abbrev: Syntax.mode -> (binding * mixfix) -> term -> term list * term list ->
-    local_theory -> local_theory
   val theory_registration: string * morphism -> (morphism * bool) option -> morphism ->
     local_theory -> local_theory
 
-  (*locale operations*)
-  val locale_notes: string -> string ->
+  (*locale target primitives*)
+  val locale_target_notes: string -> string ->
     (Attrib.binding * (thm list * Token.src list) list) list ->
     (Attrib.binding * (thm list * Token.src list) list) list ->
     local_theory -> local_theory
   val locale_target_declaration: string -> bool -> declaration -> local_theory -> local_theory
-  val locale_declaration: string -> {syntax: bool, pervasive: bool} -> declaration ->
-    local_theory -> local_theory
   val locale_target_const: string -> (morphism -> bool) -> Syntax.mode ->
     (binding * mixfix) * term -> local_theory -> local_theory
+
+  (*locale operations*)
+  val locale_declaration: string -> {syntax: bool, pervasive: bool} -> declaration ->
+    local_theory -> local_theory
   val locale_const: string -> Syntax.mode -> (binding * mixfix) * term ->
     local_theory -> local_theory
   val locale_dependency: string -> string * morphism -> (morphism * bool) option -> morphism ->
     local_theory -> local_theory
 end

 
   in (result'', result) end;
 
 in
 
-fun notes notes' kind facts lthy =
+fun notes target_notes kind facts lthy =
   let
     val facts' = facts
       |> map (fn (a, bs) => (a, Global_Theory.burrow_fact (Global_Theory.name_multi
           (Local_Theory.full_name lthy (fst a))) bs))
       |> Global_Theory.map_facts (import_export_proof lthy);
     val local_facts = Global_Theory.map_facts #1 facts';
     val global_facts = Global_Theory.map_facts #2 facts';
   in
     lthy
-    |> notes' kind global_facts (Attrib.partial_evaluation lthy local_facts)
+    |> target_notes kind global_facts (Attrib.partial_evaluation lthy local_facts)
     |> Attrib.local_notes kind local_facts
   end;
 
 end;
 
 
 (* abbrev *)
 
-fun abbrev abbrev' prmode ((b, mx), rhs) lthy =
+fun abbrev target_abbrev prmode ((b, mx), rhs) lthy =
   let
     val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy);
 
     val rhs' = Assumption.export_term lthy (Local_Theory.target_of lthy) rhs;
     val term_params = map Free (sort (Variable.fixed_ord lthy o apply2 #1) (Variable.add_fixed lthy rhs' []));

       subtract (op =) (Term.add_tfreesT (Term.fastype_of u) []) (Term.add_tfrees u []);
     val mx' = check_mixfix lthy (b, extra_tfrees) mx;
     val type_params = map (Logic.mk_type o TFree) extra_tfrees;
   in
     lthy
-    |> abbrev' prmode (b, mx') global_rhs (type_params, term_params)
+    |> target_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;
 
 
 
-(** theory operations **)
-
-fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
+(** theory target primitives **)
+
+fun theory_target_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 (op <>) Syntax.mode_default ((b, mx), lhs)
     #> pair (lhs, def));
 
-fun theory_notes kind global_facts local_facts =
+fun theory_target_notes kind global_facts local_facts =
   Local_Theory.background_theory (Attrib.global_notes kind global_facts #> snd)
   #> standard_notes (op <>) kind local_facts;
 
-fun theory_declaration decl =
-  background_declaration decl #> standard_declaration (K true) decl;
-
-fun theory_abbrev prmode (b, mx) global_rhs params =
+fun theory_target_abbrev prmode (b, mx) global_rhs params =
   Local_Theory.background_theory_result
     (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 (op <>) prmode
           ((b, if null (snd params) then NoSyn else mx), Term.list_comb (Logic.unvarify_global lhs, snd params)));
 
+
+(** theory operations **)
+
+fun theory_declaration decl =
+  background_declaration decl #> standard_declaration (K true) decl;
+
 val theory_registration =
   Local_Theory.raw_theory o Context.theory_map ooo Locale.add_registration;
 
 
 
-(** locale operations **)
-
-fun locale_notes locale kind global_facts local_facts =
+(** locale target primitives **)
+
+fun locale_target_notes locale kind global_facts local_facts =
   Local_Theory.background_theory
     (Attrib.global_notes kind (Attrib.map_facts (K []) global_facts) #> snd) #>
   (fn lthy => lthy |>
     Local_Theory.target (fn ctxt => ctxt |>
       Locale.add_thmss locale kind (standard_facts lthy ctxt local_facts))) #>

 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_target_const locale phi_pred prmode ((b, mx), rhs) =
+  locale_target_declaration locale true (const_decl phi_pred prmode ((b, mx), rhs))
+
+
+(** locale operations **)
+
 fun locale_declaration locale {syntax, pervasive} decl =
   pervasive ? background_declaration decl
   #> locale_target_declaration locale syntax decl
   #> standard_declaration (fn (_, other) => other <> 0) decl;
 
-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_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 =