anchor.diff:  let resugar_arg_qual (q:option<S.arg_qualifier>) : option<A.arg_qualifier> =
     match q with
       | None -> None
  -    | Some (Implicit b) -> Some A.Implicit  //TODO: how should we map this flag back to the surface?
  -    | Some Equality -> Some A.Equality
  +    | Some (S.Implicit b) -> Some A.Implicit  //TODO: how should we map this flag back to the surface?
  +    | Some S.Equality -> Some A.Equality
   
   let rec universe_to_int n u =
     match u with 
  
positive.code:         // make a Var term'
          A.Var (lid_of_path [a] r)
      in
      let resugar_sequence (e:A.term) : A.term =  match e.tm with
        | A.Let(_, [p, t1], t2) ->
          mk (A.Seq(t1, t2))
        | _ -> 
          failwith "This case is impossible for sequence" 
      in
      match (SS.compress t).n with //always call compress before case-analyzing a S.term
      | Tm_delayed _ ->
        failwith "This case is impossible after compress"
  
negative.code:           | Inr fv -> mk_pat (A.PatName fv.fv_name.v), term
            | Inl bv -> 
              let x, term = SS.open_term [S.mk_binder bv] term in
              let (bv, _) = List.hd x in 
              mk_pat (A.PatVar (bv_as_unique_ident bv, None)), term
          in
          if is_pat_app then
  