src/Pure/Isar/expression.ML
changeset 41585 45d7da4e4ccf
parent 41435 12585dfb86fe
child 42290 b1f544c84040
     1.1 --- a/src/Pure/Isar/expression.ML	Sat Jan 15 22:40:17 2011 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Sun Jan 16 14:57:14 2011 +0100
     1.3 @@ -29,20 +29,20 @@
     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) * ((string * typ) list * Proof.context)
     1.7 -  val add_locale: binding -> binding -> expression_i -> Element.context_i list ->
     1.8 -    theory -> string * local_theory
     1.9 -  val add_locale_cmd: binding -> binding -> expression -> Element.context list ->
    1.10 -    theory -> string * local_theory
    1.11 +  val add_locale: (local_theory -> local_theory) -> binding -> binding ->
    1.12 +    expression_i -> Element.context_i list -> theory -> string * local_theory
    1.13 +  val add_locale_cmd: (local_theory -> local_theory) -> binding -> binding ->
    1.14 +    expression -> Element.context list -> theory -> string * local_theory
    1.15  
    1.16    (* Interpretation *)
    1.17    val cert_goal_expression: expression_i -> Proof.context ->
    1.18      (term list list * (string * morphism) list * morphism) * Proof.context
    1.19    val read_goal_expression: expression -> Proof.context ->
    1.20      (term list list * (string * morphism) list * morphism) * Proof.context
    1.21 -  val sublocale: string -> expression_i -> (Attrib.binding * term) list ->
    1.22 -    theory -> Proof.state
    1.23 -  val sublocale_cmd: string -> expression -> (Attrib.binding * string) list ->
    1.24 -    theory -> Proof.state
    1.25 +  val sublocale: (local_theory -> local_theory) -> string -> expression_i ->
    1.26 +    (Attrib.binding * term) list -> theory -> Proof.state
    1.27 +  val sublocale_cmd: (local_theory -> local_theory) -> string -> expression ->
    1.28 +    (Attrib.binding * string) list -> theory -> Proof.state
    1.29    val interpretation: expression_i -> (Attrib.binding * term) list ->
    1.30      theory -> Proof.state
    1.31    val interpretation_cmd: expression -> (Attrib.binding * string) list ->
    1.32 @@ -731,7 +731,7 @@
    1.33    | defines_to_notes _ e = e;
    1.34  
    1.35  fun gen_add_locale prep_decl
    1.36 -    binding raw_predicate_binding raw_import raw_body thy =
    1.37 +    before_exit binding raw_predicate_binding raw_import raw_body thy =
    1.38    let
    1.39      val name = Sign.full_name thy binding;
    1.40      val _ = Locale.defined thy name andalso
    1.41 @@ -784,7 +784,7 @@
    1.42      val loc_ctxt = thy'
    1.43        |> Locale.register_locale binding (extraTs, params)
    1.44            (asm, rev defs) (a_intro, b_intro) axioms [] (rev notes) (rev deps')
    1.45 -      |> Named_Target.init name
    1.46 +      |> Named_Target.init before_exit name
    1.47        |> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes';
    1.48  
    1.49    in (name, loc_ctxt) end;
    1.50 @@ -900,11 +900,11 @@
    1.51            export theory) (deps ~~ witss))
    1.52    end;
    1.53  
    1.54 -fun gen_sublocale prep_expr intern parse_prop prep_attr raw_target
    1.55 -    expression equations thy =
    1.56 +fun gen_sublocale prep_expr intern parse_prop prep_attr
    1.57 +    before_exit raw_target expression equations thy =
    1.58    let
    1.59      val target = intern thy raw_target;
    1.60 -    val target_ctxt = Named_Target.init target thy;
    1.61 +    val target_ctxt = Named_Target.init before_exit target thy;
    1.62      val ((propss, deps, export), expr_ctxt) = prep_expr expression target_ctxt;
    1.63  
    1.64      val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt;
    1.65 @@ -919,8 +919,8 @@
    1.66  in
    1.67  
    1.68  fun sublocale x = gen_sublocale cert_goal_expression (K I) (K I) (K I) x;
    1.69 -fun sublocale_cmd x = gen_sublocale read_goal_expression Locale.intern
    1.70 -  Syntax.parse_prop Attrib.intern_src x;
    1.71 +fun sublocale_cmd x =
    1.72 +  gen_sublocale read_goal_expression Locale.intern Syntax.parse_prop Attrib.intern_src x;
    1.73  
    1.74  end;
    1.75