anchor.diff:  
   let mk_primed_var =
     let rec svariant avoid s =
  -    if mem s avoid || (can get_const_type s && not(is_hidden s)) then
  -      svariant avoid (s^"'")
  +    if mem s avoid || (can get_const_type s && not (is_hidden s)) then
  +      svariant avoid (s + "'")
       else s
     fun avoid v ->
  -    let s,ty = dest_var v in
  +    let s,ty = dest_var v
       let s' = svariant (mapfilter (fst << dest_var) avoid) s
       mk_var(s',ty)
   
  
positive.code: let CACHE_CONV =
      let ALPHA_HACK th =
          let tm' = lhand(concl th)
          fun tm -> if tm' = tm then th else TRANS (ALPHA tm tm') th
      fun conv ->
          let net = ref empty_net
          fun tm ->
              try tryfind (fun f -> f tm) (lookup tm (!net))
              with Failure _ ->
                  let th = conv tm
                  net := enter [] (tm,ALPHA_HACK th) (!net)
                  th
  *)
  
  
  
negative.code:     let l,r = dest_eq (concl th)
      if aconv l r then failwith "CHANGED_CONV" else th
  
  let TRY_CONV conv = ORELSEC conv ALL_CONV
  
  (* ------------------------------------------------------------------------- *)
  (* Subterm conversions.                                                      *)
  