author | haftmann |
Mon, 09 Mar 2009 10:01:58 +0100 | |
changeset 30373 | ffdd7a1f1ff0 |
parent 30372 | 96d508968153 |
child 30380 | 50eec112ca1c |
--- a/src/HOL/Library/normarith.ML Mon Mar 09 09:38:36 2009 +0100 +++ b/src/HOL/Library/normarith.ML Mon Mar 09 10:01:58 2009 +0100 @@ -873,7 +873,7 @@ fun solve (vs,eqs) = case (vs,eqs) of ([],[]) => SOME (Intfunc.onefunc (0,Rat.one)) |(_,eq::oeqs) => - (case vs inter (Intfunc.dom eq) of + (case filter (member (op =) vs) (Intfunc.dom eq) of (*FIXME use find_first here*) [] => NONE | v::_ => if Intfunc.defined eq v