diff --git a/src/boss/theory_tests/casePredScript.sml b/src/boss/theory_tests/casePredScript.sml
new file mode 100644
index 0000000000..2289e70c82
--- /dev/null
+++ b/src/boss/theory_tests/casePredScript.sml
@@ -0,0 +1,23 @@
+open HolKernel Parse boolLib bossLib;
+
+val _ = new_theory "casePred";
+
+Theorem foo:
+  (case x of [] => F | h::t => h) ==> x <> []
+Proof
+  rw[CasePred "list"]
+QED
+
+Theorem bar:
+  (case x of SOME h::t => h | _ => F) ==> x <> [NONE]
+Proof
+  rw[CasePreds ["list","option"]]
+QED
+
+Theorem baz:
+  (case x of SOME h::t => h | _ => F) ==> x <> [NONE]
+Proof
+  rw[AllCasePreds()]
+QED
+
+val _ = export_theory();