# HG changeset patch
# User wenzelm
# Date 1280852037 -7200
# Node ID ac94ff28e9e194aacfebb17a587a4d30a7b92fce
# Parent  dc65ed8bbb43d6e17d0f3fe3e8ea4f82a79ee699
eliminated Thy_Info.thy_ord, which is not really stable in interactive mode, since it depends on the somewhat accidental load order;

diff -r dc65ed8bbb43 -r ac94ff28e9e1 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Aug 03 18:10:18 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Aug 03 18:13:57 2010 +0200
@@ -391,7 +391,7 @@
     val thy = Toplevel.theory_of state;
     val thy_session = Present.session_name thy;
 
-    val all_thys = sort Thy_Info.thy_ord (thy :: Theory.ancestors_of thy);
+    val all_thys = rev (thy :: Theory.ancestors_of thy);
     val gr = all_thys |> map (fn node =>
       let
         val name = Context.theory_name node;
diff -r dc65ed8bbb43 -r ac94ff28e9e1 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Tue Aug 03 18:10:18 2010 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue Aug 03 18:13:57 2010 +0200
@@ -15,7 +15,6 @@
   val is_finished: string -> bool
   val master_directory: string -> Path.T
   val loaded_files: string -> Path.T list
-  val thy_ord: theory * theory -> order
   val remove_thy: string -> unit
   val kill_thy: string -> unit
   val use_thys: string list -> unit
@@ -144,8 +143,6 @@
   fun merge _ = empty;
 );
 
-val thy_ord = int_ord o pairself Update_Time.get;
-
 
 (* remove theory *)