tuned;
authorwenzelm
Mon, 19 Feb 2018 15:46:10 +0100
changeset 67668 23659b5dde1d
parent 67667 e0c0a6bb265b
child 67669 189c68964ab2
tuned;
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);