diff --git a/stdlib/caisar.mlw b/stdlib/caisar.mlw
index c5e157cdaa505aa3752d9eb360b14bec691075a9..8ff1b9d6e0343dcde158465466dc2994e79757de 100644
--- a/stdlib/caisar.mlw
+++ b/stdlib/caisar.mlw
@@ -24,14 +24,11 @@ theory DatasetClassification
   use ieee_float.Float64
   use int.Int
   use array.Array
-  use option.Option
 
   type features = array t
   type label_ = int
   type record = (features, label_)
   type dataset = array record
-  type ampli = { start: option int; stop: int; step: option int; }
-  type amplitude = option ampli
 
   constant dataset: dataset
 
@@ -73,7 +70,6 @@ theory DatasetClassificationProps
     correct m d /\ robust m d eps
 
   predicate meta_robust (m: model) (d: dataset) (threshold: t) (perturbation: string) (pert_path: string) (out_mode: string) (start: int) (stop: int) (step: int)
-  (* predicate meta_robust (m: model) (d: dataset) (threshold: t) (perturbation: string) (ampli: amplitude) *)
 end
 
 theory NN