src/HOL/Library/positivstellensatz.ML
changeset 39027 e4262f9e6a4e
parent 38801 319a28dd3564
child 39920 7479334d2c90
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Thu Sep 02 10:29:47 2010 +0200
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Thu Sep 02 10:29:48 2010 +0200
     1.3 @@ -549,7 +549,7 @@
     1.4  (* A linear arithmetic prover *)
     1.5  local
     1.6    val linear_add = FuncUtil.Ctermfunc.combine (curry op +/) (fn z => z =/ Rat.zero)
     1.7 -  fun linear_cmul c = FuncUtil.Ctermfunc.map (fn x => c */ x)
     1.8 +  fun linear_cmul c = FuncUtil.Ctermfunc.map (fn _ => fn x => c */ x)
     1.9    val one_tm = @{cterm "1::real"}
    1.10    fun contradictory p (e,_) = ((FuncUtil.Ctermfunc.is_empty e) andalso not(p Rat.zero)) orelse
    1.11       ((eq_set (op aconvc) (FuncUtil.Ctermfunc.dom e, [one_tm])) andalso