src/Pure/Isar/generic_target.ML

 Common target infrastructure.
 *)
 
 signature GENERIC_TARGET =
 sig
-  (*consts*)
-  val standard_const: (int * int -> bool) -> Syntax.mode -> (binding * mixfix) * term ->
-    local_theory -> local_theory
-
-  (*background operations*)
+  (*background primitives*)
   val background_foundation: ((binding * typ) * mixfix) * (binding * term) ->
     term list * term list -> local_theory -> (term * thm) * local_theory
   val background_declaration: declaration -> local_theory -> local_theory
   val background_abbrev: binding * term -> term list -> local_theory -> (term * term) * local_theory
 
-  (*lifting primitives to local theory operations*)
+  (*nested local theories primitives*)
+  val standard_const: (int * int -> bool) -> Syntax.mode -> (binding * mixfix) * term ->
+    local_theory -> local_theory
+
+  (*lifting target primitives to local theory operations*)
   val define: (((binding * typ) * mixfix) * (binding * term) ->
       term list * term list -> local_theory -> (term * thm) * local_theory) ->
     bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory
   val notes:

     local_theory -> local_theory
 end
 
 structure Generic_Target: GENERIC_TARGET =
 struct
-
-(** notes **)
-
-fun standard_facts lthy ctxt =
-  Attrib.transform_facts (Local_Theory.standard_morphism lthy ctxt);
-
-fun standard_notes pred kind facts lthy =
-  Local_Theory.map_contexts (fn level => fn ctxt =>
-    if pred (Local_Theory.level lthy, level)
-    then Attrib.local_notes kind (standard_facts lthy ctxt facts) ctxt |> snd
-    else ctxt) lthy;
-
-
-
-(** declarations **)
-
-fun standard_declaration pred decl lthy =
-  Local_Theory.map_contexts (fn level => fn ctxt =>
-    if pred (Local_Theory.level lthy, level)
-    then Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt
-    else ctxt) lthy;
-
-
 
 (** consts **)
 
 fun check_mixfix ctxt (b, extra_tfrees) mx =
   if null extra_tfrees then mx

                 (Proof_Context.generic_revert_abbrev (#1 prmode) c #>
                  Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)]))))
     end
   else context;
 
-fun standard_const pred prmode ((b, mx), rhs) =
-  standard_declaration pred (const_decl (K true) prmode ((b, mx), rhs));
-
 
 
 (** background primitives **)
 
 fun background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =

   Local_Theory.background_theory_result (Sign.add_abbrev Print_Mode.internal (b, global_rhs))
   #>> apply2 (fn t => Term.list_comb (Logic.unvarify_global t, params))
 
 
 
-(** lifting primitive to local theory operations **)
+(** nested local theories primitives **)
+
+fun standard_facts lthy ctxt =
+  Attrib.transform_facts (Local_Theory.standard_morphism lthy ctxt);
+
+fun standard_notes pred kind facts lthy =
+  Local_Theory.map_contexts (fn level => fn ctxt =>
+    if pred (Local_Theory.level lthy, level)
+    then Attrib.local_notes kind (standard_facts lthy ctxt facts) ctxt |> snd
+    else ctxt) lthy;
+
+fun standard_declaration pred decl lthy =
+  Local_Theory.map_contexts (fn level => fn ctxt =>
+    if pred (Local_Theory.level lthy, level)
+    then Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt
+    else ctxt) lthy;
+
+fun standard_const pred prmode ((b, mx), rhs) =
+  standard_declaration pred (const_decl (K true) prmode ((b, mx), rhs));
+
+
+(** lifting target primitives to local theory operations **)
 
 (* define *)
 
 fun define foundation internal ((b, mx), ((b_def, atts), rhs)) lthy =
   let