--- 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);