equal
deleted
inserted
replaced
50 let |
50 let |
51 val add = if syntax then Locale.add_syntax_declaration else Locale.add_declaration; |
51 val add = if syntax then Locale.add_syntax_declaration else Locale.add_declaration; |
52 val locale_decl = Morphism.transform (Local_Theory.target_morphism lthy) decl; |
52 val locale_decl = Morphism.transform (Local_Theory.target_morphism lthy) decl; |
53 in |
53 in |
54 lthy |
54 lthy |
55 |> pervasive ? Generic_Target.theory_declaration decl |
55 |> pervasive ? Generic_Target.theory_declaration syntax decl |
56 |> Local_Theory.target (add locale locale_decl) |
56 |> Local_Theory.target (add locale locale_decl) |
|
57 |> not syntax ? Context.proof_map (Morphism.form decl) |
57 end; |
58 end; |
58 |
59 |
59 fun target_declaration (Target {target, ...}) params = |
60 fun target_declaration (Target {target, ...}) params = |
60 if target = "" then Generic_Target.theory_declaration |
61 if target = "" then Generic_Target.theory_declaration (#syntax params) |
61 else locale_declaration target params; |
62 else locale_declaration target params; |
62 |
63 |
63 |
64 |
64 (* consts in locales *) |
65 (* consts in locales *) |
65 |
66 |