added thy_ord -- order of creation;
authorwenzelm
Thu Apr 05 00:30:31 2007 +0200 (2007-04-05)
changeset 2260376c30440c9af
parent 22602 a165d9ed08b8
child 22604 6419dcc822f1
added thy_ord -- order of creation;
ancestors: back to traditional ad-hoc order (avoid occasional problems with get_thm);
src/Pure/context.ML
     1.1 --- a/src/Pure/context.ML	Wed Apr 04 23:29:42 2007 +0200
     1.2 +++ b/src/Pure/context.ML	Thu Apr 05 00:30:31 2007 +0200
     1.3 @@ -35,6 +35,7 @@
     1.4    val str_of_thy: theory -> string
     1.5    val check_thy: theory -> theory
     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                     (*exception TERM*)
    1.11 @@ -270,6 +271,7 @@
    1.12  (* equality and inclusion *)
    1.13  
    1.14  val eq_thy = eq_id o pairself (#id o identity_of o check_thy);
    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, ...}, _, _, _)) =
    1.19 @@ -365,15 +367,13 @@
    1.20  fun maximal_thys thys =
    1.21    thys |> filter (fn thy => not (exists (fn thy' => proper_subthy (thy, thy')) thys));
    1.22  
    1.23 -val creation_order = rev_order o int_ord o pairself (#1 o #id o identity_of);
    1.24 -
    1.25  fun begin_thy pp name imports =
    1.26    if name = draftN then error ("Illegal theory name: " ^ quote draftN)
    1.27    else
    1.28      let
    1.29        val parents =
    1.30          maximal_thys (distinct eq_thy (map check_thy imports));
    1.31 -      val ancestors = sort_distinct creation_order (parents @ maps ancestors_of parents);
    1.32 +      val ancestors = distinct eq_thy (parents @ maps ancestors_of parents);
    1.33        val Theory ({id, ids, iids, ...}, data, _, _) =
    1.34          (case parents of
    1.35            [] => error "No parent theories"