src/Pure/Isar/expression.ML

       * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context)
       (*FIXME*)
   val read_declaration: expression -> (Proof.context -> Proof.context) -> Element.context list ->
     Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
       * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context)
-  val add_locale: (local_theory -> local_theory) -> binding -> binding ->
+  val add_locale: binding -> binding ->
     expression_i -> Element.context_i list -> theory -> string * local_theory
-  val add_locale_cmd: (local_theory -> local_theory) -> binding -> binding ->
+  val add_locale_cmd: binding -> binding ->
     expression -> Element.context list -> theory -> string * local_theory
 
   (* Interpretation *)
   val cert_goal_expression: expression_i -> Proof.context ->
     (term list list * (string * morphism) list * morphism) * Proof.context

   val interpretation: expression_i -> (Attrib.binding * term) list -> local_theory -> Proof.state
   val interpretation_cmd: expression -> (Attrib.binding * string) list ->
     local_theory -> Proof.state
   val sublocale: expression_i -> (Attrib.binding * term) list -> local_theory -> Proof.state
   val sublocale_cmd: expression -> (Attrib.binding * string) list -> local_theory -> Proof.state
-  val sublocale_global: (local_theory -> local_theory) -> string -> expression_i ->
+  val sublocale_global: string -> expression_i ->
     (Attrib.binding * term) list -> theory -> Proof.state
-  val sublocale_global_cmd: (local_theory -> local_theory) -> xstring * Position.T -> expression ->
+  val sublocale_global_cmd: xstring * Position.T -> expression ->
     (Attrib.binding * string) list -> theory -> Proof.state
 
   (* Diagnostic *)
   val print_dependencies: Proof.context -> bool -> expression -> unit
 end;

         (a, [([Assumption.assume ctxt (cterm_of (Proof_Context.theory_of ctxt) def)],
           [(Attrib.internal o K) Locale.witness_add])])) defs)
   | defines_to_notes _ e = e;
 
 fun gen_add_locale prep_decl
-    before_exit binding raw_predicate_binding raw_import raw_body thy =
+    binding raw_predicate_binding raw_import raw_body thy =
   let
     val name = Sign.full_name thy binding;
     val _ = Locale.defined thy name andalso
       error ("Duplicate definition of locale " ^ quote name);
 

     val axioms = map (Element.conclude_witness pred_ctxt) b_axioms;
 
     val loc_ctxt = thy'
       |> Locale.register_locale binding (extraTs, params)
           (asm, rev defs) (a_intro, b_intro) axioms [] (rev notes) (rev deps')
-      |> Named_Target.init before_exit name
+      |> Named_Target.init name
       |> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes';
 
   in (name, loc_ctxt) end;
 
 in

 
 
 (* special case: global sublocale command *)
 
 fun gen_sublocale_global prep_loc prep_interpretation
-    before_exit raw_locale expression raw_eqns thy =
-  let
-    val lthy = Named_Target.init before_exit (prep_loc thy raw_locale) thy;
+    raw_locale expression raw_eqns thy =
+  let
+    val lthy = Named_Target.init (prep_loc thy raw_locale) thy;
     fun setup_proof after_qed =
       Element.witness_proof_eqs
         (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit);
   in
     lthy |>