src/ZF/arith_data.ML
changeset 29269 5c25a2012975
parent 26287 df8e5362cff9
child 32155 e2bf2f73b0c8
     1.1 --- a/src/ZF/arith_data.ML	Wed Dec 31 00:08:14 2008 +0100
     1.2 +++ b/src/ZF/arith_data.ML	Wed Dec 31 15:30:10 2008 +0100
     1.3 @@ -1,7 +1,5 @@
     1.4  (*  Title:      ZF/arith_data.ML
     1.5 -    ID:         $Id$
     1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   2000  University of Cambridge
     1.8  
     1.9  Arithmetic simplification: cancellation of common terms
    1.10  *)
    1.11 @@ -106,7 +104,7 @@
    1.12  
    1.13  (*Dummy version: the "coefficient" is always 1.
    1.14    In the result, the factors are sorted terms*)
    1.15 -fun dest_coeff t = (1, mk_prod (sort Term.term_ord (dest_prod t)));
    1.16 +fun dest_coeff t = (1, mk_prod (sort TermOrd.term_ord (dest_prod t)));
    1.17  
    1.18  (*Find first coefficient-term THAT MATCHES u*)
    1.19  fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])