equal
deleted
inserted
replaced
191 (* init and exit *) |
191 (* init and exit *) |
192 |
192 |
193 fun begin_theory name imports uses = |
193 fun begin_theory name imports uses = |
194 ThyInfo.begin_theory Present.begin_theory name imports (map (apfst Path.unpack) uses); |
194 ThyInfo.begin_theory Present.begin_theory name imports (map (apfst Path.unpack) uses); |
195 |
195 |
196 val end_theory = (ThyInfo.check_known_thy o Context.theory_name) ? ThyInfo.end_theory; |
196 fun end_theory thy = |
|
197 if ThyInfo.check_known_thy (Context.theory_name thy) then ThyInfo.end_theory thy else thy; |
197 |
198 |
198 val kill_theory = ThyInfo.if_known_thy ThyInfo.remove_thy; |
199 val kill_theory = ThyInfo.if_known_thy ThyInfo.remove_thy; |
199 |
200 |
200 fun theory (name, imports, uses) = |
201 fun theory (name, imports, uses) = |
201 Toplevel.init_theory (begin_theory name imports uses) |
202 Toplevel.init_theory (begin_theory name imports uses) |