equal
deleted
inserted
replaced
103 (* declaration *) |
103 (* declaration *) |
104 |
104 |
105 fun declaration (Target {target, is_locale, ...}) {syntax, pervasive} decl = |
105 fun declaration (Target {target, is_locale, ...}) {syntax, pervasive} decl = |
106 if is_locale then |
106 if is_locale then |
107 pervasive ? Generic_Target.background_declaration decl |
107 pervasive ? Generic_Target.background_declaration decl |
108 #> Generic_Target.locale_declaration target syntax decl |
108 #> Generic_Target.locale_target_declaration target syntax decl |
109 #> Generic_Target.standard_declaration (fn (_, other) => other <> 0) decl |
109 #> Generic_Target.standard_declaration (fn (_, other) => other <> 0) decl |
110 else Generic_Target.theory_declaration decl; |
110 else Generic_Target.theory_declaration decl; |
111 |
111 |
112 |
112 |
113 (* subscription *) |
113 (* subscription *) |