removed thy_ord (erratic due to multi-threading);
authorwenzelm
Sat, 08 Sep 2007 19:58:35 +0200
changeset 24559 dae0972c0066
parent 24558 419f7cde7f59
child 24560 2693220bd77f
removed thy_ord (erratic due to multi-threading);
src/Pure/context.ML
--- 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, ...}, _, _, _)) =