let reify =
    let module Hash = Hashtbl.Make(
      struct
        type t = tsym * int
        let equal (f, n) (g, m) =  f == g && n = m
        let hash (f, _) = hash f
      end) 
    in
    let ht = Hash.create 17 in
    let _ = Tools.add_at_reset (fun () -> Hash.clear ht) in
      fun (f, n) ->
        assert(not(is f));
        try
          Hash.find ht (f, n)
        with
            Not_found ->
              let op = (Cl(Reify(f, n)), genidx()) in
                Hash.add ht (f, n) op; op