src/Pure/thm_name.ML
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