changeset 35408 | b48ab741683b |
parent 33317 | b4534348b8fd |
child 35409 | 5c5bb83f2bae |
--- a/src/ZF/arith_data.ML Sat Feb 27 22:52:25 2010 +0100 +++ b/src/ZF/arith_data.ML Sat Feb 27 23:13:01 2010 +0100 @@ -104,7 +104,7 @@ (*Dummy version: the "coefficient" is always 1. In the result, the factors are sorted terms*) -fun dest_coeff t = (1, mk_prod (sort TermOrd.term_ord (dest_prod t))); +fun dest_coeff t = (1, mk_prod (sort Term_Ord.term_ord (dest_prod t))); (*Find first coefficient-term THAT MATCHES u*) fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])