# HG changeset patch
# User wenzelm
# Date 1519051570 -3600
# Node ID 23659b5dde1dd3bdc476d6ff1bcb89dfec22e9e1
# Parent  e0c0a6bb265bca86159d99cf63b882c284963d5d
tuned;

diff -r e0c0a6bb265b -r 23659b5dde1d src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Mon Feb 19 15:41:17 2018 +0100
+++ b/src/Pure/Isar/locale.ML	Mon Feb 19 15:46:10 2018 +0100
@@ -59,8 +59,8 @@
   val add_declaration: string -> bool -> declaration -> Proof.context -> Proof.context
 
   (* Activation *)
+  val activate_facts: morphism option -> string * morphism -> Context.generic -> Context.generic
   val activate_declarations: string * morphism -> Proof.context -> Proof.context
-  val activate_facts: morphism option -> string * morphism -> Context.generic -> Context.generic
   val init: string -> theory -> Proof.context
 
   (* Reasoning about locales *)
@@ -455,14 +455,6 @@
 
 (** Public activation functions **)
 
-fun activate_declarations dep = Context.proof_map (fn context =>
-  context
-  |> Context_Position.set_visible_generic false
-  |> pair (Idents.get context)
-  |> roundup (Context.theory_of context) activate_syntax_decls Morphism.identity dep
-  |-> Idents.put
-  |> Context_Position.restore_visible_generic context);
-
 fun activate_facts export dep context =
   context
   |> Context_Position.set_visible_generic false
@@ -473,6 +465,14 @@
   |-> Idents.put
   |> Context_Position.restore_visible_generic context;
 
+fun activate_declarations dep = Context.proof_map (fn context =>
+  context
+  |> Context_Position.set_visible_generic false
+  |> pair (Idents.get context)
+  |> roundup (Context.theory_of context) activate_syntax_decls Morphism.identity dep
+  |-> Idents.put
+  |> Context_Position.restore_visible_generic context);
+
 fun init name thy =
   let
     val context = Context.Proof (Proof_Context.init_global thy);