anchor.diff:    (* Grobner basis algorithm.                                                *)
     (* ----------------------------------------------------------------------- *)
     
  -  let rec grobner_basis basis pairs =
  -    Format.print_string(string(length basis)+" basis elements and "+
  -                        string(length pairs)+" critical pairs");
  -    Format.print_newline();
  -    match pairs with
  -      [] -> basis
  -    | (l,(p1,p2))::opairs ->
  -          let (sp,hist as sph) = monic (reduce basis (spoly l p1 p2))
  -          if sp = [] || criterion2 basis (l,(p1,p2)) opairs
  -          then grobner_basis basis opairs else
  -          if constant_poly sp then grobner_basis (sph::basis) [] else
  -          let rawcps =
  -            map (fun p -> mlcm (hd(fst p)) (hd sp),align(p,sph)) basis
  -          let newcps = filter (fun (l,(p,q)) -> not(orthogonal l (fst p) (fst q))) rawcps
  -          grobner_basis (sph::basis)
  -                  (merge forder opairs (mergesort forder newcps))
  +  let rec grobner_basis basis pairs = 
  +      Format.print_string(string(length basis) + " basis elements and " + string(length pairs) + " critical pairs")
  +      Format.print_newline()
  +      match pairs with
  +      | [] -> basis
  +      | (l, (p1, p2)) :: opairs -> 
  +          let (sp, hist as sph) = monic(reduce basis (spoly l p1 p2))
  +          if sp = [] || criterion2 basis (l, (p1, p2)) opairs then grobner_basis basis opairs
  +          else if constant_poly sp then grobner_basis (sph :: basis) []
  +          else 
  +              let rawcps = map (fun p -> mlcm (hd(fst p)) (hd sp), align(p, sph)) basis
  +              let newcps = filter (fun (l, (p, q)) -> not(orthogonal l (fst p) (fst q))) rawcps
  +              grobner_basis (sph :: basis) (merge forder opairs (mergesort forder newcps))
     
     (* ----------------------------------------------------------------------- *)
     (* Interreduce initial polynomials.                                        *)
     (* ----------------------------------------------------------------------- *)
     
  -  let rec grobner_interreduce rpols ipols =
  -    match ipols with
  -      [] -> map monic (rev rpols)
  -    | p::ps -> let p' = reduce (rpols @ ps) p
  -               if fst p' = [] then grobner_interreduce rpols ps
  -               else grobner_interreduce (p'::rpols) ps
  +  let rec grobner_interreduce rpols ipols = 
  +      match ipols with
  +      | [] -> map monic (rev rpols)
  +      | p :: ps -> 
  +          let p' = reduce (rpols @ ps) p
  +          if fst p' = [] then grobner_interreduce rpols ps
  +          else grobner_interreduce (p' :: rpols) ps
     
     (* ----------------------------------------------------------------------- *)
     (* Overall function.                                                       *)
     (* ----------------------------------------------------------------------- *)
     
  -  let grobner pols =
  -    let npols = map2 (fun p n -> p,Start n) pols (0--(length pols - 1))
  -    let phists = filter (fun (p,_) -> p <> []) npols
  -    let bas = grobner_interreduce [] (map monic phists)
  -    let prs0 = allpairs (fun x y -> x,y) bas bas
  -    let prs1 = filter (fun ((x,_),(y,_)) -> poly_lt x y) prs0
  -    let prs2 = map (fun (p,q) -> mlcm (hd(fst p)) (hd(fst q)),(p,q)) prs1
  -    let prs3 =
  -      filter (fun (l,(p,q)) -> not(orthogonal l (fst p) (fst q))) prs2
  -    grobner_basis bas (mergesort forder prs3)
  +  let grobner pols = 
  +      let npols = map2 (fun p n -> p, Start n) pols (0 -- (length pols - 1))
  +      let phists = filter (fun (p, _) -> p <> []) npols
  +      let bas = grobner_interreduce [] (map monic phists)
  +      let prs0 = allpairs (fun x y -> x, y) bas bas
  +      let prs1 = filter (fun ((x, _), (y, _)) -> poly_lt x y) prs0
  +      let prs2 = map (fun (p, q) -> mlcm (hd(fst p)) (hd(fst q)), (p, q)) prs1
  +      let prs3 = filter (fun (l, (p, q)) -> not(orthogonal l (fst p) (fst q))) prs2
  +      grobner_basis bas (mergesort forder prs3)
     
     (* ----------------------------------------------------------------------- *)
     (* Get proof of contradiction from Grobner basis.                          *)
     (* ----------------------------------------------------------------------- *)
     
  -  let grobner_refute pols =
  -    let gb = grobner pols
  -    snd(Option.get <| find (fun (p,h) -> length p = 1 && forall ((=)0) (snd(hd p))) gb)
  +  let grobner_refute pols = 
  +      let gb = grobner pols
  +      snd(Option.get <| find (fun (p, h) -> length p = 1 && forall ((=) 0) (snd(hd p))) gb)
     
     (* ----------------------------------------------------------------------- *)
     (* Turn proof into a certificate as sum of multipliers.                    *)
  
positive.code:   let poly_eq p1 p2 =
      forall2 (fun (c1,m1) (c2,m2) -> c1 = c2 && m1 = m2) p1 p2
    
    let memx ((p1,h1),(p2,h2)) ppairs =
      not (exists (fun ((q1,_),(q2,_)) -> poly_eq p1 q1 && poly_eq p2 q2)
                  ppairs)
    
    (* ----------------------------------------------------------------------- *)
    (* Buchberger's second criterion.                                          *)
    (* ----------------------------------------------------------------------- *)
    
    let criterion2 basis (lcm,((p1,h1),(p2,h2))) opairs =
      /// Tests for failure.
      let can f x = 
          try f x |> ignore; true
          with Failure _ -> false
  
      exists (fun g -> not(poly_eq (fst g) p1) && not(poly_eq (fst g) p2) &&
                       can (mdiv lcm) (hd(fst g)) &&
                       not(memx (align(g,(p1,h1))) (map snd opairs)) &&
                       not(memx (align(g,(p2,h2))) (map snd opairs))) basis
    
    (* ----------------------------------------------------------------------- *)
    (* Test for hitting constant polynomial.                                   *)
  
negative.code:   
    let grob_neg = map (fun (c,m) -> (minus_num c,m))
    
    let rec grob_add l1 l2 = 
        match (l1, l2) with
        | ([], l2) -> l2
        | (l1, []) -> l1
        | ((c1, m1) :: o1, (c2, m2) :: o2) -> 
            if m1 = m2 then 
                let c = c1 + c2
                let rest = grob_add o1 o2
                if c = num_0 then rest
                else (c, m1) :: rest
            else if morder_lt m2 m1 then (c1, m1) :: (grob_add o1 l2)
            else (c2, m2) :: (grob_add l1 o2)
    
    let grob_sub l1 l2 = grob_add l1 (grob_neg l2)
    
  