src/HOL/Library/positivstellensatz.ML
changeset 59058 a78612c67ec0
parent 58628 fd3c96a8ca60
child 59582 0fbed69ff081
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Wed Nov 26 16:55:43 2014 +0100
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Wed Nov 26 20:05:34 2014 +0100
     1.3 @@ -64,13 +64,13 @@
     1.4  structure Symfunc = FuncFun(type key = string val ord = fast_string_ord);
     1.5  structure Termfunc = FuncFun(type key = term val ord = Term_Ord.fast_term_ord);
     1.6  
     1.7 -val cterm_ord = Term_Ord.fast_term_ord o pairself term_of
     1.8 +val cterm_ord = Term_Ord.fast_term_ord o apply2 term_of
     1.9  
    1.10  structure Ctermfunc = FuncFun(type key = cterm val ord = cterm_ord);
    1.11  
    1.12  type monomial = int Ctermfunc.table;
    1.13  
    1.14 -val monomial_ord = list_ord (prod_ord cterm_ord int_ord) o pairself Ctermfunc.dest
    1.15 +val monomial_ord = list_ord (prod_ord cterm_ord int_ord) o apply2 Ctermfunc.dest
    1.16  
    1.17  structure Monomialfunc = FuncFun(type key = monomial val ord = monomial_ord)
    1.18  
    1.19 @@ -78,7 +78,7 @@
    1.20  
    1.21  (* The ordering so we can create canonical HOL polynomials.                  *)
    1.22  
    1.23 -fun dest_monomial mon = sort (cterm_ord o pairself fst) (Ctermfunc.dest mon);
    1.24 +fun dest_monomial mon = sort (cterm_ord o apply2 fst) (Ctermfunc.dest mon);
    1.25  
    1.26  fun monomial_order (m1,m2) =
    1.27    if Ctermfunc.is_empty m2 then LESS