anchor.diff:            let ses = typecheck tcenv decls in
             match find_let_body ses with
             | None -> (QueryNOK, JsonStr "Typechecking yielded an unexpected term")
  -          | Some def -> let normalized = normalize_term tcenv def in
  +          | Some def -> let normalized = normalize_term tcenv rules def in
                          (QueryOK, JsonStr (Syntax.Print.term_to_string normalized))
           with | e -> (QueryNOK, (match FStar.Errors.issue_of_exn e with
                                   | Some issue -> JsonStr (FStar.Errors.format_issue issue)
  
positive.code:     let dummy_decl = Util.format1 "let __compute_dummy__ = (%s)" term in
      { frag_text = dummy_decl; frag_line = 0; frag_col = 0 } in
  
    let normalize_term tcenv t =
      FStar.TypeChecker.Normalize.normalize
        [FStar.TypeChecker.Normalize.Beta;
         FStar.TypeChecker.Normalize.Iota;
         FStar.TypeChecker.Normalize.Zeta;
         FStar.TypeChecker.Normalize.UnfoldUntil SS.Delta_constant;
         FStar.TypeChecker.Normalize.Inlining;
         FStar.TypeChecker.Normalize.Eager_unfolding;
         FStar.TypeChecker.Normalize.Primops]
        tcenv t in
  
    let find_let_body ses =
      match ses with
  
negative.code:                                        assoc "[location]" "line" loc |> js_int,
                                         assoc "[location]" "column" loc |> js_int)),
                                  arg "requested-info" |> js_list js_str)
             | "compute" -> Compute (arg "term" |> js_str,
                                    try_arg "rules"
                                      |> Util.map_option (js_list js_reductionrule))
             | "search" -> Search (arg "terms" |> js_str)
             | _ -> ProtocolViolation (Util.format1 "Unknown query '%s'" query) }
    with
  