1.1 --- a/src/Pure/proofterm.ML	Sat Feb 27 22:52:25 2010 +0100
     1.2 +++ b/src/Pure/proofterm.ML	Sat Feb 27 23:13:01 2010 +0100
     1.3 @@ -214,7 +214,7 @@
     1.4  
     1.5  (* proof body *)
     1.6  
     1.7 -val oracle_ord = prod_ord fast_string_ord TermOrd.fast_term_ord;
     1.8 +val oracle_ord = prod_ord fast_string_ord Term_Ord.fast_term_ord;
     1.9  fun thm_ord ((i, _): pthm, (j, _)) = int_ord (j, i);
    1.10  
    1.11  val merge_oracles = OrdList.union oracle_ord;