src/Pure/context.ML
changeset 24559 dae0972c0066
parent 24369 0cb1f4d76452
child 26413 003dd6155870
--- a/src/Pure/context.ML	Sat Sep 08 18:30:02 2007 +0200
+++ b/src/Pure/context.ML	Sat Sep 08 19:58:35 2007 +0200
@@ -36,7 +36,6 @@
   val deref: theory_ref -> theory
   val check_thy: theory -> theory_ref
   val eq_thy: theory * theory -> bool
-  val thy_ord: theory * theory -> order
   val subthy: theory * theory -> bool
   val joinable: theory * theory -> bool
   val merge: theory * theory -> theory
@@ -266,7 +265,6 @@
 (* equality and inclusion *)
 
 val eq_thy = eq_id o pairself (#id o identity_of);
-val thy_ord = int_ord o pairself (#1 o #id o identity_of);
 
 fun proper_subthy
     (Theory ({id = (i, _), ...}, _, _, _), Theory ({ids, iids, ...}, _, _, _)) =