| changeset 70586 | 57df8a85317a |
| parent 70459 | f0a445c5a82c |
| child 72060 | efb7fd4a6d1f |
--- a/src/Pure/context.ML Tue Aug 20 09:48:22 2019 +0200 +++ b/src/Pure/context.ML Tue Aug 20 11:01:05 2019 +0200 @@ -33,7 +33,7 @@ val timing: bool Unsynchronized.ref val parents_of: theory -> theory list val ancestors_of: theory -> theory list - val theory_id_ord: theory_id * theory_id -> order + val theory_id_ord: theory_id ord val theory_id_long_name: theory_id -> string val theory_id_name: theory_id -> string val theory_long_name: theory -> string