eliminated Thy_Info.thy_ord, which is not really stable in interactive mode, since it depends on the somewhat accidental load order;

--- 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;

--- 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 *)