src/Pure/context.ML

--- a/src/Pure/context.ML	Wed Apr 04 23:29:38 2007 +0200
+++ b/src/Pure/context.ML	Wed Apr 04 23:29:39 2007 +0200
@@ -365,13 +365,15 @@
 fun maximal_thys thys =
   thys |> filter (fn thy => not (exists (fn thy' => proper_subthy (thy, thy')) thys));
 
+val creation_order = rev_order o int_ord o pairself (#1 o #id o identity_of);
+
 fun begin_thy pp name imports =
   if name = draftN then error ("Illegal theory name: " ^ quote draftN)
   else
     let
       val parents =
         maximal_thys (distinct eq_thy (map check_thy imports));
-      val ancestors = distinct eq_thy (parents @ maps ancestors_of parents);
+      val ancestors = sort_distinct creation_order (parents @ maps ancestors_of parents);
       val Theory ({id, ids, iids, ...}, data, _, _) =
         (case parents of
           [] => error "No parent theories"