# HG changeset patch
# User haftmann
# Date 1433177960 -7200
# Node ID 69394731c4194de6a7dfc1abc0db40cf83080d78
# Parent  0e6742f89c038614573cf910394da1b3e28dc711
tuned order

diff -r 0e6742f89c03 -r 69394731c419 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Mon Jun 01 18:59:20 2015 +0200
+++ b/src/Pure/Isar/generic_target.ML	Mon Jun 01 18:59:20 2015 +0200
@@ -7,17 +7,17 @@
 
 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 ->
@@ -63,29 +63,6 @@
 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 =
@@ -139,9 +116,6 @@
     end
   else context;
 
-fun standard_const pred prmode ((b, mx), rhs) =
-  standard_declaration pred (const_decl (K true) prmode ((b, mx), rhs));
-
 
 
 (** background primitives **)
@@ -174,7 +148,28 @@
 
 
 
-(** 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 *)