1.1 --- a/src/Pure/proofterm.ML	Fri Sep 24 15:37:36 2010 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Fri Sep 24 15:53:13 2010 +0200
     1.3 @@ -24,8 +24,8 @@
     1.4     | Promise of serial * term * typ list
     1.5     | PThm of serial * ((string * term * typ list option) * proof_body future)
     1.6    and proof_body = PBody of
     1.7 -    {oracles: (string * term) OrdList.T,
     1.8 -     thms: (serial * (string * term * proof_body future)) OrdList.T,
     1.9 +    {oracles: (string * term) Ord_List.T,
    1.10 +     thms: (serial * (string * term * proof_body future)) Ord_List.T,
    1.11       proof: proof}
    1.12  
    1.13    val %> : proof * term -> proof
    1.14 @@ -46,9 +46,9 @@
    1.15  
    1.16    val oracle_ord: oracle * oracle -> order
    1.17    val thm_ord: pthm * pthm -> order
    1.18 -  val merge_oracles: oracle OrdList.T -> oracle OrdList.T -> oracle OrdList.T
    1.19 -  val merge_thms: pthm OrdList.T -> pthm OrdList.T -> pthm OrdList.T
    1.20 -  val all_oracles_of: proof_body -> oracle OrdList.T
    1.21 +  val merge_oracles: oracle Ord_List.T -> oracle Ord_List.T -> oracle Ord_List.T
    1.22 +  val merge_thms: pthm Ord_List.T -> pthm Ord_List.T -> pthm Ord_List.T
    1.23 +  val all_oracles_of: proof_body -> oracle Ord_List.T
    1.24    val approximate_proof_body: proof -> proof_body
    1.25  
    1.26    (** primitive operations **)
    1.27 @@ -163,8 +163,8 @@
    1.28   | Promise of serial * term * typ list
    1.29   | PThm of serial * ((string * term * typ list option) * proof_body future)
    1.30  and proof_body = PBody of
    1.31 -  {oracles: (string * term) OrdList.T,
    1.32 -   thms: (serial * (string * term * proof_body future)) OrdList.T,
    1.33 +  {oracles: (string * term) Ord_List.T,
    1.34 +   thms: (serial * (string * term * proof_body future)) Ord_List.T,
    1.35     proof: proof};
    1.36  
    1.37  type oracle = string * term;
    1.38 @@ -235,8 +235,8 @@
    1.39  val oracle_ord = prod_ord fast_string_ord Term_Ord.fast_term_ord;
    1.40  fun thm_ord ((i, _): pthm, (j, _)) = int_ord (j, i);
    1.41  
    1.42 -val merge_oracles = OrdList.union oracle_ord;
    1.43 -val merge_thms = OrdList.union thm_ord;
    1.44 +val merge_oracles = Ord_List.union oracle_ord;
    1.45 +val merge_thms = Ord_List.union thm_ord;
    1.46  
    1.47  val all_oracles_of =
    1.48    let
    1.49 @@ -259,8 +259,8 @@
    1.50          | _ => I) [prf] ([], []);
    1.51    in
    1.52      PBody
    1.53 -     {oracles = OrdList.make oracle_ord oracles,
    1.54 -      thms = OrdList.make thm_ord thms,
    1.55 +     {oracles = Ord_List.make oracle_ord oracles,
    1.56 +      thms = Ord_List.make thm_ord thms,
    1.57        proof = prf}
    1.58    end;
    1.59