src/HOL/Library/normarith.ML
changeset 36692 54b64d4ad524
parent 36587 534418d8d494
child 36717 2a72455be88b
     1.1 --- a/src/HOL/Library/normarith.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/HOL/Library/normarith.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -311,7 +311,7 @@
     1.4          in forall (fn e => evaluate f e =/ Rat.zero) flippedequations
     1.5          end
     1.6         val goodverts = filter check_solution rawverts
     1.7 -       val signfixups = map (fn n => if n mem_int  f then ~1 else 1) nvs 
     1.8 +       val signfixups = map (fn n => if member (op =) f n then ~1 else 1) nvs 
     1.9        in map (map2 (fn s => fn c => Rat.rat_of_int s */ c) signfixups) goodverts
    1.10        end
    1.11       val allverts = fold_rev append (map plausiblevertices (allsubsets nvs)) []