diff --git a/.github/workflows/check_encoding.yml b/.github/workflows/check_encoding.yml
index 8485b7a0b89d670902a56846e4ac8fc440d18bd5..1a12ddfd5fcb1522e7a1a30854b157bb10d90dad 100644
--- a/.github/workflows/check_encoding.yml
+++ b/.github/workflows/check_encoding.yml
@@ -44,7 +44,7 @@ jobs:
     # Runs a set of commands using the runners shell
     - name: install lambdapi and deps
       run: |
-        sudo apt install --yes bmake
+        sudo apt install --yes bmake ksh perl
         (cd "${GITHUB_WORKSPACE}/lambdapi/" || exit 1
          opam install .)
         eval $(opam env)
diff --git a/specs/tools/README.md b/specs/tools/README.md
index ff257bf3847d5aeb4023232d54fdcf2041234bcc..2637ab645dbd13846f3825259a6d7d37aa3b96d6 100644
--- a/specs/tools/README.md
+++ b/specs/tools/README.md
@@ -6,6 +6,7 @@ to Dedukti files.
 
 - `pvs2dk.sh`: translate a theory to a lambdapi file.
 - `lambdapi.pkg`: the module file for lambdapi (required to type check files).
+- `purify.pl`: trims unneeded data from theory specification files
 - `lambdapi.mk`: some targets and rules to typecheck lambdapi files.
 - `prelude_patches/*.diff`: patches that may be apply to the Prelude to
 	translate it.
diff --git a/specs/tools/prelude/Makefile b/specs/tools/prelude/Makefile
index 2e1b329022d32e9e48da07fd425db36312fd74a6..975170ce71f1d6429fdafe2f79084b1930da6e16 100644
--- a/specs/tools/prelude/Makefile
+++ b/specs/tools/prelude/Makefile
@@ -1,19 +1,25 @@
 PVS2DK = ../pvs2dk.sh
 LP     = lambdapi
 
-THEORIES != grep -v -E '^-|\#' theories
 PVSPATH  ?=
 
-all: dummy ${THEORIES:C/$/.lpo/}
+_THEORIES != ../purify.pl -p < theories
+_DUMMIES  != ../purify.pl -n < theories
+# We cannot cat _THEORIES and _DUMMIES because order is important
+_ALL      != ../purify.pl < theories
 
-.PHONY: dummy
-dummy:
-	./mk_dummy.sh
+all: ${_ALL:C/$/.lpo/}
+translate: ${_ALL:C/$/.lp/}
 
-translate: dummy ${THEORIES:C/$/.lp/}
+.for d in ${_DUMMIES}
+${d}.lp:
+	set -o noclobber && printf '// Dummy theory\n' > ${d}.lp
+${d}.lisp:
+	set -o noclobber && printf '(:context nil :decls nil)' > ${d}.lisp
+.endfor
 
 # For each theory, translate it and apply a patch if it exists
-.for th in ${THEORIES}
+.for th in ${_THEORIES}
 ${th}.lp:
 	PVSPATH=${PVSPATH} ${PVS2DK} -f ${PVSPATH}/lib/prelude.pvs -t ${.TARGET:R} \
 -o ${PWD}/${.TARGET} > /dev/null
diff --git a/specs/tools/prelude/README.md b/specs/tools/prelude/README.md
index 1afc71847b57c8ec9a2cdd0b992ea2e68a093f5e..8c4aea515d6446771b30da6898fef5763659988c 100644
--- a/specs/tools/prelude/README.md
+++ b/specs/tools/prelude/README.md
@@ -24,10 +24,9 @@ make functions.lpo
 ```
 
 The theories of the Prelude are registered in the file `theories`. In this file,
-each line is a theory. One-line comments can be inserted with character `#` *at
-the beginning of the line*.
+each line is a theory. One-line comments can be inserted with character `#`.
 If a theory name is prefixed with a dash `-`, the theory is not translated nor
-type-checked. Instead, an empty file is created with the name of the theory by
-`mk_dummy.sh`.  This allows to translate and type check theories that are
-defined further in the prelude, but do not depend on them, as theories of
-prelude require (syntactically) all previous prelude theories.
+type-checked. Instead, an empty file is created with the name of the theory by.
+This allows to translate and type check theories that are defined further in
+the prelude, but do not depend on them, as theories of prelude require
+(syntactically) all previous prelude theories.
diff --git a/specs/tools/prelude/mk_dummy.sh b/specs/tools/prelude/mk_dummy.sh
deleted file mode 100755
index b18503df0a6d3a9ab3376d0c4c15728923b52dfc..0000000000000000000000000000000000000000
--- a/specs/tools/prelude/mk_dummy.sh
+++ /dev/null
@@ -1,12 +0,0 @@
-#!/bin/ksh
-set -euo pipefail -o noclobber
-
-while read -r line; do
-    # Remove comments from line
-    nocom=$(print -f "$line" | sed -e 's/^\([^#]*\).*$/\1/' | tr -d '[:space:]')
-    if (print -f "${nocom}" | grep -E -q '^-'); then
-        fname="${nocom:1}"
-        [ -r "${fname}.lp" ] || printf '// Dummy theory\n' > "${fname}.lp"
-        [ -r "${fname}.lisp" ] || printf '(:context nil :decls nil)' > "${fname}.lisp"
-    fi
-done < 'theories'
diff --git a/specs/tools/prelude/theories b/specs/tools/prelude/theories
index 319511d04e4eec4f43fb2ef2327ed65d59ca07da..79a103186c53a38186274bcc2d07387f29877ff6 100644
--- a/specs/tools/prelude/theories
+++ b/specs/tools/prelude/theories
@@ -44,7 +44,7 @@ function_props
 -function_props_alt # Only overloading
 function_props2
 relation_defs
--relation_props
+-relation_props # Overload the composition operator
 -relation_props2
 relation_converse_props
 indexed_sets
@@ -82,7 +82,7 @@ nat_fun_props
 -restrict_set_props # Depends on finite_sets
 -extend_set_props # Depends on finite_sets
 -function_image_aux # Depends on finite_sets
--function_iterate # Recursive function definition
+function_iterate
 sequences
 seq_functions
 -finite_sequences # Use dependent records
diff --git a/specs/tools/purify.pl b/specs/tools/purify.pl
new file mode 100755
index 0000000000000000000000000000000000000000..2b656522f02b3b441d93a42985d42965e13a9ca5
--- /dev/null
+++ b/specs/tools/purify.pl
@@ -0,0 +1,36 @@
+#!/usr/bin/perl
+use strict;
+use warnings;
+
+=pod
+
+=head1 Theory specification sanitiser
+
+This script sanitises a theory specification. The flag C<-n> selects negative
+lines (lines preceded with a -) while the flac C<-p> selects positive lines
+(not preceded with a -). If no flag is given, all lines are printed and
+sanitised.
+
+=cut
+
+use Getopt::Std;
+getopts('np');
+our($opt_n, $opt_p);
+
+map {
+	$_ =~ s/#.*$//;
+	$_ =~ s/^\s+//;
+	$_ =~ s/\s+$//;
+	if ($opt_n && /^-/) {
+		# Print negative theories
+		$_ =~ s/^-(.*)$/$1/;
+		print "$_\n";
+	} elsif ($opt_p) {
+		# Print positive theories
+		print "$_\n" if /^[^-]/;
+	} elsif (! ($opt_n || $opt_p)) {
+		# Print all theories
+		$_ =~ s/^-?(.*)$/$1/;
+		print "$_\n";
+	}
+} <>;