equal
deleted
inserted
replaced
53 in |
53 in |
54 lthy |
54 lthy |
55 |> Local_Theory.target (add locale locale_decl) |
55 |> Local_Theory.target (add locale locale_decl) |
56 end; |
56 end; |
57 |
57 |
58 fun target_declaration (Target {target, ...}) {syntax, pervasive} decl = |
58 fun target_declaration (Target {target, ...}) {syntax, pervasive} decl lthy = |
59 if target = "" then Generic_Target.theory_declaration decl |
59 if target = "" then Generic_Target.theory_declaration decl lthy |
60 else |
60 else |
61 locale_declaration target syntax decl |
61 lthy |
62 #> pervasive ? Generic_Target.theory_declaration decl |
62 |> pervasive ? Local_Theory.background_theory |
63 #> not pervasive ? Context.proof_map (Morphism.form decl); |
63 (Context.theory_map |
|
64 (Morphism.form (Morphism.transform (Local_Theory.global_morphism lthy) decl))) |
|
65 |> locale_declaration target syntax decl |
|
66 |> Context.proof_map (Morphism.form decl); |
64 |
67 |
65 |
68 |
66 (* consts in locales *) |
69 (* consts in locales *) |
67 |
70 |
68 fun locale_const (ta as Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) = |
71 fun locale_const (ta as Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) = |