2 files changed, 8 insertions, 0 deletions
diff --git a/etc/isa/multiple/Err.ML b/etc/isa/multiple/Err.ML
new file mode 100644
index 00000000..177da5ce
--- /dev/null
+++ b/etc/isa/multiple/Err.ML
@@ -0,0 +1,5 @@
+(* Test to see that scripting is *not* turned on
+   if an error occurs during activation
+*)
+
+val x = 1;
diff --git a/etc/isa/multiple/Err.thy b/etc/isa/multiple/Err.thy
new file mode 100644
index 00000000..d36a5af2
--- /dev/null
+++ b/etc/isa/multiple/Err.thy
@@ -0,0 +1,3 @@
+(* Dummy file to cause an error in use_thy *)
+
+Err = blah
+\ No newline at end of file