diff --git a/src/driver/autodetection.ml b/src/driver/autodetection.ml
index 30f3158934ab09ad2534f720b3d4248be780a515..8bafdeb9d9b1e65d3c2be812a0d1e84aab373534 100644
--- a/src/driver/autodetection.ml
+++ b/src/driver/autodetection.ml
@@ -328,7 +328,7 @@ let generate_auto_strategies config =
      if b then eprintf "  Prover %a will be used in Auto level >= %d@."
                        Whyconf.print_prover p lev) prover_auto_levels;
   (* Split VCs *)
-  let code = "t split_intros_goal_wp exit" in
+  let code = "t split_vc exit" in
   let split = {
       strategy_name = "Split_VC";
       strategy_desc = "Split@ the@ VC@ into@ subgoals";
diff --git a/src/transform/introduction.ml b/src/transform/introduction.ml
index cc8d695eae5c82f26d966f9b3deaad4413b2b935..62afbbbe90aa482bd7525949c89175147b653acd 100644
--- a/src/transform/introduction.ml
+++ b/src/transform/introduction.ml
@@ -105,23 +105,9 @@ let () = Trans.register_transform
 let simplify_intros =
   Trans.compose Simplify_formula.simplify_trivial_wp_quantification introduce_premises
 
-let split_intros_goal_wp =
+let split_vc =
   Trans.compose_l Split_goal.split_goal_right (Trans.singleton simplify_intros)
 
-let split_intros_all_wp =
-  Trans.compose_l Split_goal.split_all_right (Trans.singleton simplify_intros)
-
-let split_intros_premise_wp =
-  Trans.compose Split_goal.split_premise_right simplify_intros
-
 let () = Trans.register_transform_l
-           "split_intros_goal_wp" split_intros_goal_wp
+           "split_vcp" split_vc
            ~desc:"The@ recommended@ splitting@ transformation@ to@ apply@ on@ VCs@ generated@ by@ WP@ (split_goal_right@ followed@ by@ simplify_trivial_quantifications@ followed@ by@ introduce_premises)."
-
-let () = Trans.register_transform_l
-           "split_intros_all_wp" split_intros_all_wp
-           ~desc:"Same@ as@ split_intros_goal_wp,@ but@ also@ split@ premises."
-
-let () = Trans.register_transform
-           "split_intros_premise_wp" split_intros_premise_wp
-           ~desc:"Same@ as@ split_intros_all_wp,@ but@ split@ only@ premises."
diff --git a/src/trywhy3/why3_worker.ml b/src/trywhy3/why3_worker.ml
index bfea0f1f1c244bb7c85dd60e6504476a64cfa2ee..b3471e993d0cd68287ab5c56a4bd0310db2d69b7 100644
--- a/src/trywhy3/why3_worker.ml
+++ b/src/trywhy3/why3_worker.ml
@@ -56,7 +56,7 @@ let alt_ergo_driver : Driver.driver =
 
 let () = log_time ("Initialising why3 worker: end ")
 
-let split_trans = Trans.lookup_transform_l "split_intros_goal_wp" env
+let split_trans = Trans.lookup_transform_l "split_vc" env
 
 (* CF gmain.ml ligne 568 et suivante *)
 module W =