src/Pure/Isar/generic_target.ML
author wenzelm
Fri Mar 06 15:58:56 2015 +0100 (2015-03-06)
changeset 59621 291934bac95e
parent 59616 eb59c6968219
child 60283 c927fa99d045
permissions -rw-r--r--
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm@41959
     1
(*  Title:      Pure/Isar/generic_target.ML
haftmann@38309
     2
    Author:     Makarius
haftmann@38309
     3
    Author:     Florian Haftmann, TU Muenchen
haftmann@38309
     4
haftmann@38309
     5
Common target infrastructure.
haftmann@38309
     6
*)
haftmann@38309
     7
haftmann@38309
     8
signature GENERIC_TARGET =
haftmann@38309
     9
sig
haftmann@57190
    10
  (* consts *)
haftmann@57192
    11
  val standard_const: (int * int -> bool) -> Syntax.mode -> (binding * mixfix) * term ->
haftmann@57190
    12
    local_theory -> local_theory
haftmann@57190
    13
haftmann@57190
    14
  (* background operations *)
haftmann@57190
    15
  val background_foundation: ((binding * typ) * mixfix) * (binding * term) ->
haftmann@57190
    16
    term list * term list -> local_theory -> (term * thm) * local_theory
haftmann@57190
    17
  val background_declaration: declaration -> local_theory -> local_theory
haftmann@57190
    18
  val background_abbrev: binding * term -> term list -> local_theory -> (term * term) * local_theory
haftmann@57190
    19
haftmann@57190
    20
  (* lifting primitives to local theory operations *)
wenzelm@40782
    21
  val define: (((binding * typ) * mixfix) * (binding * term) ->
wenzelm@40782
    22
      term list * term list -> local_theory -> (term * thm) * local_theory) ->
wenzelm@46992
    23
    bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
wenzelm@40782
    24
    (term * (string * thm)) * local_theory
wenzelm@47250
    25
  val notes:
wenzelm@58011
    26
    (string -> (Attrib.binding * (thm list * Token.src list) list) list ->
wenzelm@58011
    27
      (Attrib.binding * (thm list * Token.src list) list) list -> local_theory -> local_theory) ->
wenzelm@58011
    28
    string -> (Attrib.binding * (thm list * Token.src list) list) list -> local_theory ->
wenzelm@40782
    29
    (string * thm list) list * local_theory
haftmann@57118
    30
  val abbrev: (string * bool -> binding * mixfix -> term ->
haftmann@57160
    31
      term list * term list -> local_theory -> local_theory) ->
wenzelm@47250
    32
    string * bool -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory
haftmann@57190
    33
haftmann@57190
    34
  (* theory operations *)
wenzelm@40782
    35
  val theory_foundation: ((binding * typ) * mixfix) * (binding * term) ->
wenzelm@40782
    36
    term list * term list -> local_theory -> (term * thm) * local_theory
wenzelm@47250
    37
  val theory_notes: string ->
wenzelm@58011
    38
    (Attrib.binding * (thm list * Token.src list) list) list ->
wenzelm@58011
    39
    (Attrib.binding * (thm list * Token.src list) list) list ->
wenzelm@40782
    40
    local_theory -> local_theory
haftmann@57190
    41
  val theory_declaration: declaration -> local_theory -> local_theory
haftmann@57160
    42
  val theory_abbrev: Syntax.mode -> (binding * mixfix) -> term -> term list * term list ->
wenzelm@47286
    43
    local_theory -> local_theory
haftmann@52153
    44
  val theory_registration: string * morphism -> (morphism * bool) option -> morphism ->
haftmann@52153
    45
    local_theory -> local_theory
haftmann@57190
    46
haftmann@57190
    47
  (* locale operations *)
haftmann@57190
    48
  val locale_notes: string -> string ->
wenzelm@58011
    49
    (Attrib.binding * (thm list * Token.src list) list) list ->
wenzelm@58011
    50
    (Attrib.binding * (thm list * Token.src list) list) list ->
haftmann@57190
    51
    local_theory -> local_theory
haftmann@57192
    52
  val locale_target_declaration: string -> bool -> declaration -> local_theory -> local_theory
haftmann@57193
    53
  val locale_declaration: string -> {syntax: bool, pervasive: bool} -> declaration ->
haftmann@57193
    54
    local_theory -> local_theory
haftmann@57192
    55
  val locale_target_const: string -> (morphism -> bool) -> Syntax.mode ->
haftmann@57190
    56
    (binding * mixfix) * term -> local_theory -> local_theory
haftmann@57190
    57
  val locale_const: string -> Syntax.mode -> (binding * mixfix) * term ->
haftmann@57190
    58
    local_theory -> local_theory
haftmann@52153
    59
  val locale_dependency: string -> string * morphism -> (morphism * bool) option -> morphism ->
haftmann@52153
    60
    local_theory -> local_theory
wenzelm@45353
    61
end
haftmann@38309
    62
haftmann@38309
    63
structure Generic_Target: GENERIC_TARGET =
haftmann@38309
    64
struct
haftmann@38309
    65
haftmann@57191
    66
(** notes **)
haftmann@57190
    67
haftmann@57190
    68
fun standard_facts lthy ctxt =
wenzelm@58028
    69
  Attrib.transform_facts (Local_Theory.standard_morphism lthy ctxt);
haftmann@38341
    70
haftmann@57191
    71
fun standard_notes pred kind facts lthy =
haftmann@57191
    72
  Local_Theory.map_contexts (fn level => fn ctxt =>
haftmann@57191
    73
    if pred (Local_Theory.level lthy, level)
haftmann@57191
    74
    then Attrib.local_notes kind (standard_facts lthy ctxt facts) ctxt |> snd
haftmann@57191
    75
    else ctxt) lthy;
haftmann@57191
    76
haftmann@57191
    77
haftmann@57191
    78
(** declarations **)
haftmann@57191
    79
haftmann@57190
    80
fun standard_declaration pred decl lthy =
haftmann@57190
    81
  Local_Theory.map_contexts (fn level => fn ctxt =>
haftmann@57190
    82
    if pred (Local_Theory.level lthy, level)
haftmann@57190
    83
    then Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt
haftmann@57190
    84
    else ctxt) lthy;
haftmann@57190
    85
haftmann@57190
    86
haftmann@57190
    87
(** consts **)
haftmann@38312
    88
haftmann@38312
    89
fun check_mixfix ctxt (b, extra_tfrees) mx =
haftmann@38312
    90
  if null extra_tfrees then mx
haftmann@38312
    91
  else
wenzelm@56294
    92
   (if Context_Position.is_visible ctxt then
wenzelm@56294
    93
      warning
wenzelm@56294
    94
        ("Additional type variable(s) in specification of " ^ Binding.print b ^ ": " ^
wenzelm@56294
    95
          commas (map (Syntax.string_of_typ ctxt o TFree) (sort_wrt #1 extra_tfrees)) ^
wenzelm@56294
    96
          (if mx = NoSyn then ""
wenzelm@56294
    97
           else "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx)))
wenzelm@56294
    98
    else (); NoSyn);
haftmann@38312
    99
wenzelm@47291
   100
fun check_mixfix_global (b, no_params) mx =
wenzelm@47291
   101
  if no_params orelse mx = NoSyn then mx
wenzelm@47291
   102
  else (warning ("Dropping global mixfix syntax: " ^ Binding.print b ^ " " ^
wenzelm@47291
   103
    Pretty.string_of (Mixfix.pretty_mixfix mx)); NoSyn);
wenzelm@47291
   104
haftmann@57190
   105
fun const_decl phi_pred prmode ((b, mx), rhs) phi context =
haftmann@57190
   106
  if phi_pred phi then
haftmann@57190
   107
    let
haftmann@57190
   108
      val b' = Morphism.binding phi b;
haftmann@57190
   109
      val rhs' = Morphism.term phi rhs;
haftmann@57190
   110
      val same_shape = Term.aconv_untyped (rhs, rhs');
haftmann@57190
   111
      val const_alias =
haftmann@57190
   112
        if same_shape then
haftmann@57190
   113
          (case rhs' of
haftmann@57190
   114
            Const (c, T) =>
haftmann@57190
   115
              let
haftmann@57190
   116
                val thy = Context.theory_of context;
haftmann@57190
   117
                val ctxt = Context.proof_of context;
haftmann@57190
   118
              in
haftmann@57190
   119
                (case Type_Infer_Context.const_type ctxt c of
haftmann@57190
   120
                  SOME T' => if Sign.typ_equiv thy (T, T') then SOME c else NONE
haftmann@57190
   121
                | NONE => NONE)
haftmann@57190
   122
              end
haftmann@57190
   123
          | _ => NONE)
haftmann@57190
   124
        else NONE;
haftmann@57190
   125
    in
haftmann@57190
   126
      case const_alias of
haftmann@57190
   127
        SOME c =>
haftmann@57190
   128
          context
haftmann@57190
   129
          |> Context.mapping (Sign.const_alias b' c) (Proof_Context.const_alias b' c)
haftmann@57190
   130
          |> Morphism.form (Proof_Context.generic_notation true prmode [(rhs', mx)])
haftmann@57190
   131
      | NONE =>
haftmann@57190
   132
          context
haftmann@57190
   133
          |> Proof_Context.generic_add_abbrev Print_Mode.internal (b', Term.close_schematic_term rhs')
haftmann@57190
   134
          |-> (fn (const as Const (c, _), _) => same_shape ?
haftmann@57190
   135
                (Proof_Context.generic_revert_abbrev (#1 prmode) c #>
haftmann@57190
   136
                 Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)])))
haftmann@57190
   137
    end
haftmann@57190
   138
  else context;
haftmann@57190
   139
haftmann@57192
   140
fun standard_const pred prmode ((b, mx), rhs) =
haftmann@57190
   141
  standard_declaration pred (const_decl (K true) prmode ((b, mx), rhs));
haftmann@57190
   142
haftmann@57190
   143
haftmann@57190
   144
(** background primitives **)
haftmann@57190
   145
haftmann@57190
   146
fun background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
haftmann@57190
   147
  let
haftmann@57190
   148
    val params = type_params @ term_params;
haftmann@57190
   149
    val mx' = check_mixfix_global (b, null params) mx;
haftmann@57190
   150
haftmann@57190
   151
    val (const, lthy2) = lthy
haftmann@57190
   152
      |> Local_Theory.background_theory_result (Sign.declare_const lthy ((b, U), mx'));
haftmann@57190
   153
    val lhs = Term.list_comb (const, params);
haftmann@57190
   154
haftmann@57190
   155
    val ((_, def), lthy3) = lthy2
haftmann@57190
   156
      |> Local_Theory.background_theory_result
haftmann@57190
   157
        (Thm.add_def lthy2 false false
haftmann@57190
   158
          (Thm.def_binding_optional b b_def, Logic.mk_equals (lhs, rhs)));
haftmann@57190
   159
  in ((lhs, def), lthy3) end;
haftmann@57190
   160
haftmann@57190
   161
fun background_declaration decl lthy =
haftmann@57190
   162
  let
haftmann@57190
   163
    val theory_decl =
haftmann@57190
   164
      Local_Theory.standard_form lthy
haftmann@57190
   165
        (Proof_Context.init_global (Proof_Context.theory_of lthy)) decl;
haftmann@57190
   166
  in Local_Theory.background_theory (Context.theory_map theory_decl) lthy end;
haftmann@57190
   167
haftmann@57190
   168
fun background_abbrev (b, global_rhs) params =
haftmann@57190
   169
  Local_Theory.background_theory_result (Sign.add_abbrev Print_Mode.internal (b, global_rhs))
wenzelm@59058
   170
  #>> apply2 (fn t => Term.list_comb (Logic.unvarify_global t, params))
haftmann@57190
   171
haftmann@57190
   172
haftmann@57190
   173
(** lifting primitive to local theory operations **)
haftmann@38312
   174
haftmann@38309
   175
(* define *)
haftmann@38309
   176
wenzelm@46992
   177
fun define foundation internal ((b, mx), ((b_def, atts), rhs)) lthy =
haftmann@38309
   178
  let
wenzelm@59616
   179
    val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy);
haftmann@38309
   180
haftmann@38309
   181
    (*term and type parameters*)
wenzelm@59621
   182
    val ((defs, _), rhs') = Thm.cterm_of lthy rhs
wenzelm@47276
   183
      |> Local_Defs.export_cterm lthy thy_ctxt ||> Thm.term_of;
haftmann@38309
   184
wenzelm@47272
   185
    val xs = Variable.add_fixed lthy rhs' [];
haftmann@38309
   186
    val T = Term.fastype_of rhs;
haftmann@38309
   187
    val tfreesT = Term.add_tfreesT T (fold (Term.add_tfreesT o #2) xs []);
haftmann@38309
   188
    val extra_tfrees = rev (subtract (op =) tfreesT (Term.add_tfrees rhs []));
haftmann@38312
   189
    val mx' = check_mixfix lthy (b, extra_tfrees) mx;
haftmann@38309
   190
haftmann@38309
   191
    val type_params = map (Logic.mk_type o TFree) extra_tfrees;
wenzelm@59058
   192
    val term_params = map Free (sort (Variable.fixed_ord lthy o apply2 #1) xs);
haftmann@38309
   193
    val params = type_params @ term_params;
haftmann@38309
   194
haftmann@38309
   195
    val U = map Term.fastype_of params ---> T;
haftmann@38309
   196
haftmann@38309
   197
    (*foundation*)
wenzelm@45353
   198
    val ((lhs', global_def), lthy2) = lthy
wenzelm@45353
   199
      |> foundation (((b, U), mx'), (b_def, rhs')) (type_params, term_params);
haftmann@38309
   200
haftmann@38309
   201
    (*local definition*)
haftmann@38315
   202
    val ((lhs, local_def), lthy3) = lthy2
haftmann@38309
   203
      |> Local_Defs.add_def ((b, NoSyn), lhs');
wenzelm@47240
   204
wenzelm@47240
   205
    (*result*)
wenzelm@47238
   206
    val def =
wenzelm@47240
   207
      Thm.transitive local_def global_def
wenzelm@59621
   208
      |> Local_Defs.contract lthy3 defs (Thm.cterm_of lthy3 (Logic.mk_equals (lhs, rhs)));
haftmann@38315
   209
    val ([(res_name, [res])], lthy4) = lthy3
wenzelm@47080
   210
      |> Local_Theory.notes [((if internal then Binding.empty else b_def, atts), [([def], [])])];
haftmann@38315
   211
  in ((lhs, (res_name, res)), lthy4) end;
haftmann@38309
   212
haftmann@38309
   213
haftmann@38309
   214
(* notes *)
haftmann@38309
   215
wenzelm@47250
   216
local
wenzelm@47250
   217
haftmann@38309
   218
fun import_export_proof ctxt (name, raw_th) =
haftmann@38309
   219
  let
wenzelm@59616
   220
    val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of ctxt);
haftmann@38309
   221
haftmann@38309
   222
    (*export assumes/defines*)
wenzelm@54883
   223
    val th = Goal.norm_result ctxt raw_th;
wenzelm@45407
   224
    val ((defs, asms), th') = Local_Defs.export ctxt thy_ctxt th;
wenzelm@54742
   225
    val asms' = map (rewrite_rule ctxt (Drule.norm_hhf_eqs @ defs)) asms;
haftmann@38309
   226
haftmann@38309
   227
    (*export fixes*)
haftmann@38309
   228
    val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []);
haftmann@38309
   229
    val frees = map Free (Thm.fold_terms Term.add_frees th' []);
wenzelm@45352
   230
    val (th'' :: vs) =
wenzelm@59621
   231
      (th' :: map (Drule.mk_term o Thm.cterm_of ctxt) (map Logic.mk_type tfrees @ frees))
haftmann@38309
   232
      |> Variable.export ctxt thy_ctxt
haftmann@38309
   233
      |> Drule.zero_var_indexes_list;
haftmann@38309
   234
haftmann@38309
   235
    (*thm definition*)
wenzelm@45413
   236
    val result = Global_Theory.name_thm true true name th'';
haftmann@38309
   237
haftmann@38309
   238
    (*import fixes*)
haftmann@38309
   239
    val (tvars, vars) =
haftmann@38309
   240
      chop (length tfrees) (map (Thm.term_of o Drule.dest_term) vs)
haftmann@38309
   241
      |>> map Logic.dest_type;
haftmann@38309
   242
haftmann@38309
   243
    val instT = map_filter (fn (TVar v, T) => SOME (v, T) | _ => NONE) (tvars ~~ tfrees);
haftmann@38309
   244
    val inst = filter (is_Var o fst) (vars ~~ frees);
wenzelm@59616
   245
    val cinstT = instT
wenzelm@59621
   246
      |> map (apply2 (Thm.ctyp_of ctxt) o apfst TVar);
wenzelm@59616
   247
    val cinst = inst
wenzelm@59621
   248
      |> map (apply2 (Thm.cterm_of ctxt o Term.map_types (Term_Subst.instantiateT instT)));
haftmann@38309
   249
    val result' = Thm.instantiate (cinstT, cinst) result;
haftmann@38309
   250
haftmann@38309
   251
    (*import assumes/defines*)
haftmann@38309
   252
    val result'' =
wenzelm@45407
   253
      (fold (curry op COMP) asms' result'
wenzelm@45407
   254
        handle THM _ => raise THM ("Failed to re-import result", 0, result' :: asms'))
wenzelm@54742
   255
      |> Local_Defs.contract ctxt defs (Thm.cprop_of th)
wenzelm@54883
   256
      |> Goal.norm_result ctxt
wenzelm@39557
   257
      |> Global_Theory.name_thm false false name;
haftmann@38309
   258
haftmann@38309
   259
  in (result'', result) end;
haftmann@38309
   260
wenzelm@47250
   261
in
wenzelm@47250
   262
haftmann@57192
   263
fun notes notes' kind facts lthy =
haftmann@38309
   264
  let
haftmann@38309
   265
    val facts' = facts
wenzelm@39557
   266
      |> map (fn (a, bs) => (a, Global_Theory.burrow_fact (Global_Theory.name_multi
haftmann@38309
   267
          (Local_Theory.full_name lthy (fst a))) bs))
wenzelm@39557
   268
      |> Global_Theory.map_facts (import_export_proof lthy);
wenzelm@39557
   269
    val local_facts = Global_Theory.map_facts #1 facts';
wenzelm@39557
   270
    val global_facts = Global_Theory.map_facts #2 facts';
haftmann@38309
   271
  in
haftmann@38309
   272
    lthy
haftmann@57192
   273
    |> notes' kind global_facts (Attrib.partial_evaluation lthy local_facts)
wenzelm@47249
   274
    |> Attrib.local_notes kind local_facts
haftmann@38309
   275
  end;
haftmann@38309
   276
wenzelm@47250
   277
end;
wenzelm@47250
   278
haftmann@38309
   279
haftmann@38309
   280
(* abbrev *)
haftmann@38309
   281
haftmann@57192
   282
fun abbrev abbrev' prmode ((b, mx), rhs) lthy =
haftmann@38309
   283
  let
wenzelm@42360
   284
    val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy);
haftmann@38309
   285
haftmann@57109
   286
    val rhs' = Assumption.export_term lthy (Local_Theory.target_of lthy) rhs;
wenzelm@59058
   287
    val term_params = map Free (sort (Variable.fixed_ord lthy o apply2 #1) (Variable.add_fixed lthy rhs' []));
haftmann@57160
   288
    val u = fold_rev lambda term_params rhs';
wenzelm@47290
   289
    val global_rhs = singleton (Variable.polymorphic thy_ctxt) u;
haftmann@38309
   290
haftmann@38309
   291
    val extra_tfrees =
haftmann@38309
   292
      subtract (op =) (Term.add_tfreesT (Term.fastype_of u) []) (Term.add_tfrees u []);
haftmann@38312
   293
    val mx' = check_mixfix lthy (b, extra_tfrees) mx;
haftmann@57160
   294
    val type_params = map (Logic.mk_type o TFree) extra_tfrees;
haftmann@38309
   295
  in
haftmann@38309
   296
    lthy
haftmann@57192
   297
    |> abbrev' prmode (b, mx') global_rhs (type_params, term_params)
haftmann@57109
   298
    |> Proof_Context.add_abbrev Print_Mode.internal (b, rhs) |> snd
haftmann@57109
   299
    |> Local_Defs.fixed_abbrev ((b, NoSyn), rhs)
haftmann@38309
   300
  end;
haftmann@38309
   301
haftmann@38341
   302
haftmann@57190
   303
(** theory operations **)
haftmann@38341
   304
wenzelm@47284
   305
fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
wenzelm@47284
   306
  background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params)
haftmann@57192
   307
  #-> (fn (lhs, def) => standard_const (op <>) Syntax.mode_default ((b, mx), lhs)
haftmann@57057
   308
    #> pair (lhs, def));
wenzelm@47284
   309
wenzelm@47250
   310
fun theory_notes kind global_facts local_facts =
haftmann@57191
   311
  Local_Theory.background_theory (Attrib.global_notes kind global_facts #> snd)
haftmann@57191
   312
  #> standard_notes (op <>) kind local_facts;
haftmann@38341
   313
haftmann@57190
   314
fun theory_declaration decl =
haftmann@57190
   315
  background_declaration decl #> standard_declaration (K true) decl;
haftmann@57190
   316
haftmann@57118
   317
fun theory_abbrev prmode (b, mx) global_rhs params =
wenzelm@47286
   318
  Local_Theory.background_theory_result
haftmann@57109
   319
    (Sign.add_abbrev (#1 prmode) (b, global_rhs) #->
wenzelm@47291
   320
      (fn (lhs, _) =>  (* FIXME type_params!? *)
haftmann@57160
   321
        Sign.notation true prmode [(lhs, check_mixfix_global (b, null (snd params)) mx)] #> pair lhs))
haftmann@57192
   322
  #-> (fn lhs => standard_const (op <>) prmode
haftmann@57160
   323
          ((b, if null (snd params) then NoSyn else mx), Term.list_comb (Logic.unvarify_global lhs, snd params)));
haftmann@38341
   324
haftmann@57190
   325
val theory_registration =
haftmann@57190
   326
  Local_Theory.raw_theory o Context.theory_map ooo Locale.add_registration;
haftmann@57190
   327
haftmann@57190
   328
haftmann@57190
   329
(** locale operations **)
haftmann@57190
   330
haftmann@57190
   331
fun locale_notes locale kind global_facts local_facts =
haftmann@57190
   332
  Local_Theory.background_theory
haftmann@57190
   333
    (Attrib.global_notes kind (Attrib.map_facts (K []) global_facts) #> snd) #>
haftmann@57190
   334
  (fn lthy => lthy |>
haftmann@57190
   335
    Local_Theory.target (fn ctxt => ctxt |>
haftmann@57190
   336
      Locale.add_thmss locale kind (standard_facts lthy ctxt local_facts))) #>
haftmann@57191
   337
  standard_notes (fn (this, other) => other <> 0 andalso this <> other) kind local_facts;
haftmann@57190
   338
haftmann@57192
   339
fun locale_target_declaration locale syntax decl lthy = lthy
haftmann@57190
   340
  |> Local_Theory.target (fn ctxt => ctxt |>
haftmann@57190
   341
    Locale.add_declaration locale syntax
haftmann@57190
   342
      (Morphism.transform (Local_Theory.standard_morphism lthy ctxt) decl));
haftmann@57190
   343
haftmann@57193
   344
fun locale_declaration locale {syntax, pervasive} decl =
haftmann@57193
   345
  pervasive ? background_declaration decl
haftmann@57193
   346
  #> locale_target_declaration locale syntax decl
haftmann@57193
   347
  #> standard_declaration (fn (_, other) => other <> 0) decl;
haftmann@57193
   348
haftmann@57192
   349
fun locale_target_const locale phi_pred prmode ((b, mx), rhs) =
haftmann@57192
   350
  locale_target_declaration locale true (const_decl phi_pred prmode ((b, mx), rhs))
haftmann@57190
   351
haftmann@57190
   352
fun locale_const locale prmode ((b, mx), rhs) =
haftmann@57192
   353
  locale_target_const locale (K true) prmode ((b, mx), rhs)
haftmann@57192
   354
  #> standard_const (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, mx), rhs);
haftmann@57190
   355
haftmann@57190
   356
fun locale_dependency locale dep_morph mixin export =
haftmann@57190
   357
  (Local_Theory.raw_theory ooo Locale.add_dependency locale) dep_morph mixin export
wenzelm@57926
   358
  #> Locale.activate_fragment_nonbrittle dep_morph mixin export;
wenzelm@47279
   359
haftmann@38309
   360
end;