Remove cv_rep_add and use [cv_rep] annotation instead

A big thank you to @digama0 for tracking down this bug. The bug
made it so that cv_trans_deep_embedding only stored the cv_rep
theorems in the local theory and they were not accessible from
other theories.

src/num/theories/cv_compute/automation/cv_memLib.sig

@@ -19,7 +19,6 @@ sig
   val cv_inline_thms  : unit -> thm list
   val cv_from_to_thms : unit -> thm list
 
-  val cv_rep_add      : thm -> unit
   val cv_pre_add      : thm -> unit
   val cv_inline_add   : thm -> unit
   val cv_from_to_add  : thm -> unit

src/num/theories/cv_compute/automation/cv_memLib.sml

@@ -116,7 +116,7 @@ fun prepare th = let
  *--------------------------------------------------------------------------*)
 
 fun insert_cv_rep th = prepare th;
-val (cv_rep_thms, cv_rep_add) = register_ThmSetData_list "cv_rep" insert_cv_rep;
+val (cv_rep_thms, _) = register_ThmSetData_list "cv_rep" insert_cv_rep;
 
 fun insert_cv_pre th = (
   cv_print Verbose "\ncv_pre:\n\n";

src/num/theories/cv_compute/automation/cv_transLib.sml

@@ -805,7 +805,7 @@ fun cv_trans_deep_embedding eval_conv th =
       val _ = DefnBase.register_defn {tag="user", thmname=eq_name}
       val num_0 = cvSyntax.mk_cv_num (numSyntax.term_of_int 0)
       val cv_trans_thm = defn_thm |> INST [x |-> num_0] |> SYM
-      val _ = cv_memLib.cv_rep_add cv_trans_thm
+      val _ = save_thm(nm ^ "_cv_thm[cv_rep]",cv_trans_thm)
   in () end
 
 (*--------------------------------------------------------------------------*