anchor.diff:        (t1|> term_to_string)
         (match ret_opt with
          | None -> ""
  -       | Some ret -> Util.format1 "ret %s " (term_to_string ret))
  +       | Some (as_opt, ret) ->
  +         Util.format2 "%sreturns %s "
  +           (match as_opt with
  +            | None -> ""
  +            | Some as_ident -> Util.format1 " as %s " (string_of_id as_ident))
  +           (term_to_string ret))
         (t2|> term_to_string)
         (t3|> term_to_string)
   
  
positive.code:   | ElimOr of term * term * term * binder * term * binder * term  (* elim_or P Q to R with x.e1 and y.e2 *)
    | ElimAnd of term * term * term * binder * binder * term        (* elim_and P Q to R with x y. e *)
  and term = {tm:term'; range:range; level:level}
  
  and patterns = list<ident> * list<list<term>>
  
  
negative.code:     (scrutinee|> term_to_string)
      (match ret_opt with
       | None -> ""
       | Some (as_opt, ret) ->
         Util.format2 "%sreturns %s "
           (match as_opt with
            | None -> ""
            | Some as_ident -> Util.format1 "as %s " (string_of_id as_ident))
           (term_to_string ret))
      (to_string_l " | " (fun (p,w,e) -> Util.format3 "%s %s -> %s"
        (p |> pat_to_string)
        (match w with | None -> "" | Some e -> Util.format1 "when %s" (term_to_string e))
  