# HG changeset patch # User haftmann # Date 1283420560 -7200 # Node ID 548e933b90ad2eef466487886bdc28f498865bab # Parent b27d6643591c111e91a6b150459ddee53a446e1d Table.map replaces Table.map' diff -r b27d6643591c -r 548e933b90ad src/HOL/Multivariate_Analysis/normarith.ML --- a/src/HOL/Multivariate_Analysis/normarith.ML Thu Sep 02 10:33:13 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/normarith.ML Thu Sep 02 11:42:40 2010 +0200 @@ -32,16 +32,16 @@ (Thm.dest_arg t) acc | _ => augment_norm true t acc - val cterm_lincomb_neg = FuncUtil.Ctermfunc.map Rat.neg + val cterm_lincomb_neg = FuncUtil.Ctermfunc.map (K Rat.neg) fun cterm_lincomb_cmul c t = - if c =/ Rat.zero then FuncUtil.Ctermfunc.empty else FuncUtil.Ctermfunc.map (fn x => x */ c) t + if c =/ Rat.zero then FuncUtil.Ctermfunc.empty else FuncUtil.Ctermfunc.map (fn _ => fn x => x */ c) t fun cterm_lincomb_add l r = FuncUtil.Ctermfunc.combine (curry op +/) (fn x => x =/ Rat.zero) l r fun cterm_lincomb_sub l r = cterm_lincomb_add l (cterm_lincomb_neg r) fun cterm_lincomb_eq l r = FuncUtil.Ctermfunc.is_empty (cterm_lincomb_sub l r) - val int_lincomb_neg = FuncUtil.Intfunc.map Rat.neg + val int_lincomb_neg = FuncUtil.Intfunc.map (K Rat.neg) fun int_lincomb_cmul c t = - if c =/ Rat.zero then FuncUtil.Intfunc.empty else FuncUtil.Intfunc.map (fn x => x */ c) t + if c =/ Rat.zero then FuncUtil.Intfunc.empty else FuncUtil.Intfunc.map (fn _ => fn x => x */ c) t fun int_lincomb_add l r = FuncUtil.Intfunc.combine (curry op +/) (fn x => x =/ Rat.zero) l r fun int_lincomb_sub l r = int_lincomb_add l (int_lincomb_neg r) fun int_lincomb_eq l r = FuncUtil.Intfunc.is_empty (int_lincomb_sub l r)