equal
deleted
inserted
replaced
473 end |
473 end |
474 | ord => ord) |
474 | ord => ord) |
475 and hd_ord (f, g) = (* ~ term.ML *) |
475 and hd_ord (f, g) = (* ~ term.ML *) |
476 prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g) |
476 prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g) |
477 and terms_ord str pr (ts, us) = |
477 and terms_ord str pr (ts, us) = |
478 list_ord (term_ord' pr (assoc_thy "Isac.thy"))(ts, us); |
478 list_ord (term_ord' pr (assoc_thy "Isac"))(ts, us); |
479 in |
479 in |
480 |
480 |
481 fun ord_make_polynomial (pr:bool) thy (_:subst) tu = |
481 fun ord_make_polynomial (pr:bool) thy (_:subst) tu = |
482 (term_ord' pr thy(***) tu = LESS ); |
482 (term_ord' pr thy(***) tu = LESS ); |
483 |
483 |