# HG changeset patch
# User wenzelm
# Date 1333396323 -7200
# Node ID d2367cc84235dad877f70e942773ab3248be88b5
# Parent  4bab649dedf0762c761ffcd6cac75aac144d56ce
tuned;

diff -r 4bab649dedf0 -r d2367cc84235 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Mon Apr 02 21:49:27 2012 +0200
+++ b/src/Pure/Isar/generic_target.ML	Mon Apr 02 21:52:03 2012 +0200
@@ -24,8 +24,8 @@
       term list -> local_theory -> local_theory) ->
     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 locale_declaration: string -> bool -> declaration -> 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 ->
@@ -210,15 +210,15 @@
         (Proof_Context.init_global (Proof_Context.theory_of lthy)) decl;
   in Local_Theory.background_theory (Context.theory_map theory_decl) lthy end;
 
-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 locale_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 standard_declaration decl lthy =
+  Local_Theory.map_contexts (fn _ => fn ctxt =>
+    Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt) lthy;
+
 
 
 (** primitive theory operations **)