diff --git a/src/bin/common/parse_command.ml b/src/bin/common/parse_command.ml
index 5d83f65b1..d5fa49d20 100644
--- a/src/bin/common/parse_command.ml
+++ b/src/bin/common/parse_command.ml
@@ -1509,21 +1509,22 @@ let parse_theory_opt =
       Term.(const mk_disable_theories $ disable_theories $ disable_adts $ no_ac)
     in
     let preludes enable_theories disable_theories =
-      let theories = Theories.default in
+      let theories = Theories.Set.of_list Theories.default in
       let rec aux th en dis =
         match en, dis with
-        | _ :: _, [] -> aux (List.rev_append en th) [] []
+        | _ :: _, [] ->
+          aux (List.fold_left (fun th en -> Theories.Set.add en th) th en) [] []
         | e :: _, d :: _ when e = d ->
           Fmt.error_msg "theory prelude '%a' cannot be both enabled and
           disabled" Theories.pp e
-        | e :: en, d :: _ when e < d -> aux (e :: th) en dis
-        | _ , d :: dis -> aux (List.filter ((<>) d) th) en dis
-        | [], [] -> Ok th
+        | e :: en, d :: _ when e < d -> aux (Theories.Set.add e th) en dis
+        | _ , d :: dis -> aux (Theories.Set.filter ((<>) d) th) en dis
+        | [], [] -> Ok (Theories.Set.elements th)
       in
       aux
         theories
-        (List.fast_sort compare enable_theories)
-        (List.fast_sort compare disable_theories)
+        (List.fast_sort Theories.compare enable_theories)
+        (List.fast_sort Theories.compare disable_theories)
     in
     Term.(
       cli_parse_result (
diff --git a/src/lib/util/theories.ml b/src/lib/util/theories.ml
index 8e2aaf32f..2c39ca2c6 100644
--- a/src/lib/util/theories.ml
+++ b/src/lib/util/theories.ml
@@ -16,19 +16,43 @@
 (*                                                                        *)
 (**************************************************************************)
 
-type prelude = Fpa | Ria | Nra [@@deriving eq]
+type prelude = Nra | Ria | Fpa [@@deriving eq]
 
 let pp_prelude ppf = function
   | Fpa -> Format.fprintf ppf "fpa"
   | Ria -> Format.fprintf ppf "ria"
   | Nra -> Format.fprintf ppf "nra"
 
+let compare_prelude p1 p2 =
+  match p1, p2 with
+  | Nra, Nra -> 0
+  | Nra, _ -> -1
+  | _, Nra -> 1
+
+  | Ria, Ria -> 0
+  | Ria, _ -> -1
+  | _, Ria -> 1
+
+  | Fpa, Fpa -> 0
+
 type t =
   | Prelude of prelude
   | ADT
   | AC
 [@@deriving eq]
 
+let compare t1 t2 =
+  match t1, t2 with
+  | Prelude p1, Prelude p2 -> compare_prelude p1 p2
+  | Prelude _, _ -> -1
+  | _, Prelude _ -> 1
+
+  | ADT, ADT -> 0
+  | ADT, _ -> -1
+  | _, ADT -> 1
+
+  | AC, AC -> 0
+
 let pp ppf = function
   | Prelude p -> pp_prelude ppf p
   | ADT -> Format.fprintf ppf "adt"
@@ -52,3 +76,5 @@ let default = all
 
 let preludes =
   List.filter_map (function | Prelude p -> Some p | _ -> None)
+
+module Set = Set.Make(struct type nonrec t = t let compare = compare end)