anchor.diff:              if op = "forall" then mk (A.QForall([], [[]], resugar_term body))
               else mk (A.QExists([], [[]], resugar_term body))
             in
  -          (* only the last two args are from original AST terms, others are added by typechecker *)
  +          (* only the last arg is from original AST terms, others are added by typechecker *)
             (* TODO: we need a place to store the information in the args added by the typechecker *)
  -          let args = last args in
  -          begin match args with
  -            | [(b, _)] -> resugar b
  -            | _ -> failwith "wrong args format to QForall"
  -          end
  +          if List.length args > 0 then
  +            let args = last args in
  +            begin match args with
  +              | [(b, _)] -> resugar b
  +              | _ -> failwith "wrong args format to QForall"
  +            end
  +          else 
  +            resugar_as_app e args
   
           | Some "alloc" ->
             let (e, _ ) = List.hd args in
  
positive.code: module D = FStar.Parser.ToDocument
  
  let bv_as_unique_ident (x:S.bv) : I.ident =
    let unique_name =  x.ppname.idText in
    I.mk_ident (unique_name, x.ppname.idRange)
  
  let resugar_arg_qual (q:option<S.arg_qualifier>) : option<A.arg_qualifier> =
    match q with
  
negative.code:           let resugar body = match (SS.compress body).n with
              | Tm_abs(xs, body, _) ->
                  let xs, body = SS.open_term xs body in
                  let xs = if (Options.print_implicits()) then xs else filter_imp xs in
                  let xs = xs |> List.map (fun (b, qual) -> resugar_bv_as_binder b t.pos) in
                  let pats, body = match (SS.compress body).n with
                    | Tm_meta(e, m) ->
  