From 40f6b6ec497fb013a51e0ee0e6928e9bc0af26ab Mon Sep 17 00:00:00 2001
From: Michael Norrish <michael.norrish@nicta.com.au>
Date: Tue, 2 Jun 2015 21:30:58 +1000
Subject: [PATCH] Improved test-cases for record redefinition bug

For github issue #260
---
 src/datatype/theory_tests/bar260Script.sml |  4 ++++
 src/datatype/theory_tests/foo260Script.sml |  4 ++++
 src/datatype/theory_tests/gh260aScript.sml |  8 --------
 src/datatype/theory_tests/gh260bScript.sml | 10 ----------
 4 files changed, 8 insertions(+), 18 deletions(-)
 create mode 100644 src/datatype/theory_tests/bar260Script.sml
 create mode 100644 src/datatype/theory_tests/foo260Script.sml
 delete mode 100644 src/datatype/theory_tests/gh260aScript.sml
 delete mode 100644 src/datatype/theory_tests/gh260bScript.sml

diff --git a/src/datatype/theory_tests/bar260Script.sml b/src/datatype/theory_tests/bar260Script.sml
new file mode 100644
index 0000000000..f5ad0dce19
--- /dev/null
+++ b/src/datatype/theory_tests/bar260Script.sml
@@ -0,0 +1,4 @@
+open HolKernel Datatype foo260Theory;
+val _ = new_theory"bar260";
+val _ = Datatype`foo = <| f : bool |>`;
+val _ = export_theory();
diff --git a/src/datatype/theory_tests/foo260Script.sml b/src/datatype/theory_tests/foo260Script.sml
new file mode 100644
index 0000000000..ff06070bb2
--- /dev/null
+++ b/src/datatype/theory_tests/foo260Script.sml
@@ -0,0 +1,4 @@
+open HolKernel Datatype
+val _ = new_theory"foo260";
+val _ = Datatype`foo = <| f : bool |>`;
+val _ = export_theory();
diff --git a/src/datatype/theory_tests/gh260aScript.sml b/src/datatype/theory_tests/gh260aScript.sml
deleted file mode 100644
index e6737687ba..0000000000
--- a/src/datatype/theory_tests/gh260aScript.sml
+++ /dev/null
@@ -1,8 +0,0 @@
-open HolKernel Parse boolLib Datatype
-
-val _ = new_theory "gh260a";
-
-val _ = Datatype`foo = <| fld : num |>`;
-
-
-val _ = export_theory();
diff --git a/src/datatype/theory_tests/gh260bScript.sml b/src/datatype/theory_tests/gh260bScript.sml
deleted file mode 100644
index bd389fe343..0000000000
--- a/src/datatype/theory_tests/gh260bScript.sml
+++ /dev/null
@@ -1,10 +0,0 @@
-open HolKernel Parse boolLib Datatype
-
-open gh260aTheory
-
-val _ = new_theory "gh260b";
-
-val _ = Datatype`foo = <| fld : num |>`
-
-
-val _ = export_theory();