removed thy_ord (erratic due to multi-threading);
authorwenzelm
Sat Sep 08 19:58:35 2007 +0200 (2007-09-08)
changeset 24559dae0972c0066
parent 24558 419f7cde7f59
child 24560 2693220bd77f
removed thy_ord (erratic due to multi-threading);
src/Pure/context.ML
     1.1 --- a/src/Pure/context.ML	Sat Sep 08 18:30:02 2007 +0200
     1.2 +++ b/src/Pure/context.ML	Sat Sep 08 19:58:35 2007 +0200
     1.3 @@ -36,7 +36,6 @@
     1.4    val deref: theory_ref -> theory
     1.5    val check_thy: theory -> theory_ref
     1.6    val eq_thy: theory * theory -> bool
     1.7 -  val thy_ord: theory * theory -> order
     1.8    val subthy: theory * theory -> bool
     1.9    val joinable: theory * theory -> bool
    1.10    val merge: theory * theory -> theory
    1.11 @@ -266,7 +265,6 @@
    1.12  (* equality and inclusion *)
    1.13  
    1.14  val eq_thy = eq_id o pairself (#id o identity_of);
    1.15 -val thy_ord = int_ord o pairself (#1 o #id o identity_of);
    1.16  
    1.17  fun proper_subthy
    1.18      (Theory ({id = (i, _), ...}, _, _, _), Theory ({ids, iids, ...}, _, _, _)) =