# HG changeset patch
# User haftmann
# Date 1236589318 -3600
# Node ID ffdd7a1f1ff0200ab665b0bd0deccf71bde74356
# Parent  96d508968153b371ce8cbfe8cd9e0499fdd3df2a
attempt to bypass spurious infix syntax problem on polyml/sun

diff -r 96d508968153 -r ffdd7a1f1ff0 src/HOL/Library/normarith.ML
--- 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