equal
deleted
inserted
replaced
168 |
168 |
169 (* join theory *) |
169 (* join theory *) |
170 |
170 |
171 fun join_theory [] = raise List.Empty |
171 fun join_theory [] = raise List.Empty |
172 | join_theory [thy] = thy |
172 | join_theory [thy] = thy |
173 | join_theory thys = foldl1 Context.join_thys thys |> Sign.restore_naming (hd thys); |
173 | join_theory thys = foldl1 Context.join_thys thys; |
174 |
174 |
175 |
175 |
176 (* begin/end theory *) |
176 (* begin/end theory *) |
177 |
177 |
178 val begin_wrappers = rev o #1 o #wrappers o rep_theory; |
178 val begin_wrappers = rev o #1 o #wrappers o rep_theory; |
191 val thy = Context.begin_thy name imports; |
191 val thy = Context.begin_thy name imports; |
192 val wrappers = begin_wrappers thy; |
192 val wrappers = begin_wrappers thy; |
193 in |
193 in |
194 thy |
194 thy |
195 |> init_markup (name, pos) |
195 |> init_markup (name, pos) |
|
196 |> Sign.init_naming |
196 |> Sign.local_path |
197 |> Sign.local_path |
197 |> Sign.theory_naming |
|
198 |> apply_wrappers wrappers |
198 |> apply_wrappers wrappers |
199 |> tap (Syntax.force_syntax o Sign.syn_of) |
199 |> tap (Syntax.force_syntax o Sign.syn_of) |
200 end; |
200 end; |
201 |
201 |
202 fun end_theory thy = |
202 fun end_theory thy = |