src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML
changeset 33339 d41f77196338
parent 33030 2f4b36efa95e
child 37744 3daaf23b9ab4
     1.1 --- a/src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML	Thu Oct 29 23:49:55 2009 +0100
     1.2 +++ b/src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML	Thu Oct 29 23:56:33 2009 +0100
     1.3 @@ -100,7 +100,7 @@
     1.4    (fn (x, k) => (cterm_of (ProofContext.theory_of ctxt) (Free (x, @{typ real})), k)) 
     1.5  
     1.6  fun parse_monomial ctxt = repeat_sep "*" (parse_varpow ctxt) >>
     1.7 -  List.foldl (uncurry FuncUtil.Ctermfunc.update) FuncUtil.Ctermfunc.empty
     1.8 +  (fn xs => fold FuncUtil.Ctermfunc.update xs FuncUtil.Ctermfunc.empty)
     1.9  
    1.10  fun parse_cmonomial ctxt =
    1.11    rat_int --| str "*" -- (parse_monomial ctxt) >> swap ||
    1.12 @@ -108,7 +108,7 @@
    1.13    rat_int >> (fn r => (FuncUtil.Ctermfunc.empty, r))
    1.14  
    1.15  fun parse_poly ctxt = repeat_sep "+" (parse_cmonomial ctxt) >>
    1.16 -  List.foldl (uncurry FuncUtil.Monomialfunc.update) FuncUtil.Monomialfunc.empty
    1.17 +  (fn xs => fold FuncUtil.Monomialfunc.update xs FuncUtil.Monomialfunc.empty)
    1.18  
    1.19  (* positivstellensatz parser *)
    1.20