A test-case demonstrating the problem with github issue #115.

Currently failing so I've put this onto a branch of its own.

src/boss/theory_tests/github115aScript.sml

@@ -0,0 +1,14 @@
+open HolKernel Parse boolLib bossLib
+
+val _ = new_theory "github115a"
+
+open arithmeticTheory
+
+val _ = overload_on ("foo", ``\x. x + y``)
+
+val sample = store_thm(
+  "sample",
+  ``!y:bool. foo x < foo z ==> x < z``,
+  SRW_TAC [ARITH_ss][])
+
+val _ = export_theory()

src/boss/theory_tests/github115bScript.sml

@@ -0,0 +1,15 @@
+open HolKernel Parse boolLib bossLib
+
+open github115aTheory
+
+(* this theory is in the test-case solely to force Holmake to check that the
+   github115aTheory.sml file is loadable (it isn't when the bug is evident
+   because the exception in the execution of export_theory results in a
+   corrupt Theory.sml file)
+*)
+
+val _ = new_theory "github115b"
+
+val sample2 = save_thm("sample2", AND_CLAUSES)
+
+val _ = export_theory()