Improved test-cases for record redefinition bug

For github issue #260
HOL-Theorem-Prover · Jun 2, 2015 · 40f6b6e · 40f6b6e
1 parent abc8e74
commit 40f6b6e
Show file tree

Hide file tree

Showing 4 changed files with 8 additions and 18 deletions.
diff --git a/src/datatype/theory_tests/bar260Script.sml 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
@@ -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
diff --git a/src/datatype/theory_tests/gh260bScript.sml b/src/datatype/theory_tests/gh260bScript.sml