anchor.diff:  let GENERAL_REWRITE_CONV rep (cnvl : conv -> conv) (builtin_net : gconv net) thl = 
       let thl_canon = itlist (mk_rewrites false) thl []
       let final_net = itlist (net_of_thm rep) thl_canon builtin_net
  -    cnvl(REWRITES_CONV final_net)
  +    let foo1 = REWRITES_CONV final_net
  +    cnvl foo1
   
   /// Rewrites a term, selecting terms according to a user-specified strategy.
   let GEN_REWRITE_CONV (cnvl : conv -> conv) thl = 
  
positive.code: (* Abbreviation tactics.                                                     *)
  (* ------------------------------------------------------------------------- *)
  /// Tactic to introduce an abbreviation.
  let ABBREV_TAC tm = 
      let cvs, t = Choice.get <| dest_eq tm
      let v, vs = strip_comb cvs
      let rs = list_mk_abs(vs, t)
  
negative.code: // basic_congs: Lists the congruence rules used by the simplifier.
  let set_basic_congs, extend_basic_congs, basic_congs = 
      let congs = ref([] : thm list)
      (fun thl -> congs := thl),
      (fun thl -> congs := union' equals_thm thl (!congs)),
      (fun () -> !congs)
  
  (* ------------------------------------------------------------------------- *)
  (* Main rewriting conversions.                                               *)
  