diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/FORMULA.sig b/lib/forgejo.ballcloud.cc/wball/proof-checker/kernel/FORMULA.sig
similarity index 100%
rename from lib/forgejo.ballcloud.cc/wball/proof-checker/FORMULA.sig
rename to lib/forgejo.ballcloud.cc/wball/proof-checker/kernel/FORMULA.sig
diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/Formula.sml b/lib/forgejo.ballcloud.cc/wball/proof-checker/kernel/Formula.sml
similarity index 100%
rename from lib/forgejo.ballcloud.cc/wball/proof-checker/Formula.sml
rename to lib/forgejo.ballcloud.cc/wball/proof-checker/kernel/Formula.sml
diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/PROOF.sig b/lib/forgejo.ballcloud.cc/wball/proof-checker/kernel/PROOF.sig
similarity index 100%
rename from lib/forgejo.ballcloud.cc/wball/proof-checker/PROOF.sig
rename to lib/forgejo.ballcloud.cc/wball/proof-checker/kernel/PROOF.sig
diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/Proof.sml b/lib/forgejo.ballcloud.cc/wball/proof-checker/kernel/Proof.sml
similarity index 100%
rename from lib/forgejo.ballcloud.cc/wball/proof-checker/Proof.sml
rename to lib/forgejo.ballcloud.cc/wball/proof-checker/kernel/Proof.sml
diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/TERM.sig b/lib/forgejo.ballcloud.cc/wball/proof-checker/kernel/TERM.sig
similarity index 100%
rename from lib/forgejo.ballcloud.cc/wball/proof-checker/TERM.sig
rename to lib/forgejo.ballcloud.cc/wball/proof-checker/kernel/TERM.sig
diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/Term.sml b/lib/forgejo.ballcloud.cc/wball/proof-checker/kernel/Term.sml
similarity index 100%
rename from lib/forgejo.ballcloud.cc/wball/proof-checker/Term.sml
rename to lib/forgejo.ballcloud.cc/wball/proof-checker/kernel/Term.sml
diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/VAR.sig b/lib/forgejo.ballcloud.cc/wball/proof-checker/kernel/VAR.sig
similarity index 100%
rename from lib/forgejo.ballcloud.cc/wball/proof-checker/VAR.sig
rename to lib/forgejo.ballcloud.cc/wball/proof-checker/kernel/VAR.sig
diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/Var.sml b/lib/forgejo.ballcloud.cc/wball/proof-checker/kernel/Var.sml
similarity index 100%
rename from lib/forgejo.ballcloud.cc/wball/proof-checker/Var.sml
rename to lib/forgejo.ballcloud.cc/wball/proof-checker/kernel/Var.sml
diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/kernel/kernel.mlb b/lib/forgejo.ballcloud.cc/wball/proof-checker/kernel/kernel.mlb
new file mode 100644
index 0000000..b3f85dc
--- /dev/null
+++ b/lib/forgejo.ballcloud.cc/wball/proof-checker/kernel/kernel.mlb
@@ -0,0 +1,9 @@
+$(SML_LIB)/basis/basis.mlb
+VAR.sig
+Var.sml
+TERM.sig
+Term.sml
+FORMULA.sig
+Formula.sml
+PROOF.sig
+Proof.sml
diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/parser.mlb b/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/parser.mlb
new file mode 100644
index 0000000..2c35957
--- /dev/null
+++ b/lib/forgejo.ballcloud.cc/wball/proof-checker/parser/parser.mlb
@@ -0,0 +1,3 @@
+$(SML_LIB)/basis/basis.mlb
+../../../../github.com/diku-dk/sml-parse/parse.mlb
+../../../../github.com/diku-dk/sml-parse/simple_token.mlb
diff --git a/lib/forgejo.ballcloud.cc/wball/proof-checker/proof-checker.mlb b/lib/forgejo.ballcloud.cc/wball/proof-checker/proof-checker.mlb
index 7fb49f1..6485e94 100644
--- a/lib/forgejo.ballcloud.cc/wball/proof-checker/proof-checker.mlb
+++ b/lib/forgejo.ballcloud.cc/wball/proof-checker/proof-checker.mlb
@@ -1,11 +1,2 @@
 $(SML_LIB)/basis/basis.mlb
-../../../github.com/diku-dk/sml-parse/parse.mlb
-../../../github.com/diku-dk/sml-parse/simple_token.mlb
-VAR.sig
-Var.sml
-TERM.sig
-Term.sml
-FORMULA.sig
-Formula.sml
-PROOF.sig
-Proof.sml
+kernel/kernel.mlb