changeset 70586 | 57df8a85317a |
parent 70575 | bf1a59014481 |
child 79329 | 992c494bda25 |
--- a/src/Pure/thm_name.ML Tue Aug 20 09:48:22 2019 +0200 +++ b/src/Pure/thm_name.ML Tue Aug 20 11:01:05 2019 +0200 @@ -10,7 +10,7 @@ signature THM_NAME = sig type T = string * int - val ord: T * T -> order + val ord: T ord val print: T -> string val flatten: T -> string val make_list: string -> thm list -> (T * thm) list