src/Pure/Isar/expression.ML
changeset 57181 2d13bf9ea77b
parent 56809 b60009672a65
child 57860 bcc243ea48e7
     1.1 --- a/src/Pure/Isar/expression.ML	Fri Jun 06 12:36:06 2014 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Fri Jun 06 19:19:46 2014 +0200
     1.3 @@ -31,9 +31,9 @@
     1.4    val read_declaration: expression -> (Proof.context -> Proof.context) -> Element.context list ->
     1.5      Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
     1.6        * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context)
     1.7 -  val add_locale: (local_theory -> local_theory) -> binding -> binding ->
     1.8 +  val add_locale: binding -> binding ->
     1.9      expression_i -> Element.context_i list -> theory -> string * local_theory
    1.10 -  val add_locale_cmd: (local_theory -> local_theory) -> binding -> binding ->
    1.11 +  val add_locale_cmd: binding -> binding ->
    1.12      expression -> Element.context list -> theory -> string * local_theory
    1.13  
    1.14    (* Interpretation *)
    1.15 @@ -53,9 +53,9 @@
    1.16      local_theory -> Proof.state
    1.17    val sublocale: expression_i -> (Attrib.binding * term) list -> local_theory -> Proof.state
    1.18    val sublocale_cmd: expression -> (Attrib.binding * string) list -> local_theory -> Proof.state
    1.19 -  val sublocale_global: (local_theory -> local_theory) -> string -> expression_i ->
    1.20 +  val sublocale_global: string -> expression_i ->
    1.21      (Attrib.binding * term) list -> theory -> Proof.state
    1.22 -  val sublocale_global_cmd: (local_theory -> local_theory) -> xstring * Position.T -> expression ->
    1.23 +  val sublocale_global_cmd: xstring * Position.T -> expression ->
    1.24      (Attrib.binding * string) list -> theory -> Proof.state
    1.25  
    1.26    (* Diagnostic *)
    1.27 @@ -762,7 +762,7 @@
    1.28    | defines_to_notes _ e = e;
    1.29  
    1.30  fun gen_add_locale prep_decl
    1.31 -    before_exit binding raw_predicate_binding raw_import raw_body thy =
    1.32 +    binding raw_predicate_binding raw_import raw_body thy =
    1.33    let
    1.34      val name = Sign.full_name thy binding;
    1.35      val _ = Locale.defined thy name andalso
    1.36 @@ -820,7 +820,7 @@
    1.37      val loc_ctxt = thy'
    1.38        |> Locale.register_locale binding (extraTs, params)
    1.39            (asm, rev defs) (a_intro, b_intro) axioms [] (rev notes) (rev deps')
    1.40 -      |> Named_Target.init before_exit name
    1.41 +      |> Named_Target.init name
    1.42        |> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes';
    1.43  
    1.44    in (name, loc_ctxt) end;
    1.45 @@ -938,9 +938,9 @@
    1.46  (* special case: global sublocale command *)
    1.47  
    1.48  fun gen_sublocale_global prep_loc prep_interpretation
    1.49 -    before_exit raw_locale expression raw_eqns thy =
    1.50 +    raw_locale expression raw_eqns thy =
    1.51    let
    1.52 -    val lthy = Named_Target.init before_exit (prep_loc thy raw_locale) thy;
    1.53 +    val lthy = Named_Target.init (prep_loc thy raw_locale) thy;
    1.54      fun setup_proof after_qed =
    1.55        Element.witness_proof_eqs
    1.56          (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit);