# HG changeset patch
# User wenzelm
# Date 1175722179 -7200
# Node ID d920d38f1f02a942c480ef8ffc594f13a3b9d811
# Parent  f31a869077f0b405c5a0d2c35d59e5e4650645b9
theory: maintain ancestors in order of creation;

diff -r f31a869077f0 -r d920d38f1f02 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"