# HG changeset patch
# User nipkow
# Date 797496463 -7200
# Node ID 23190112d369ce38621517e4781a049d15771f12
# Parent  b860420000350983ad21c0d37c3fbe9b805d285b
Removed the "exit 1" calls, since now the Makefile does them.

diff -r b86042000035 -r 23190112d369 src/HOL/IMP/ROOT.ML
--- a/src/HOL/IMP/ROOT.ML	Mon Apr 10 08:40:58 1995 +0200
+++ b/src/HOL/IMP/ROOT.ML	Mon Apr 10 08:47:43 1995 +0200
@@ -19,7 +19,6 @@
 writeln"Root file for CHOL/IMP";
 proof_timing := true;
 loadpath := [".","IMP"];
-(time_use_thy "Properties";
- time_use_thy "Equiv";
- time_use_thy "Hoare"
-) handle _ => exit 1;
+time_use_thy "Properties";
+time_use_thy "Equiv";
+time_use_thy "Hoare";
diff -r b86042000035 -r 23190112d369 src/HOL/IOA/ROOT.ML
--- a/src/HOL/IOA/ROOT.ML	Mon Apr 10 08:40:58 1995 +0200
+++ b/src/HOL/IOA/ROOT.ML	Mon Apr 10 08:47:43 1995 +0200
@@ -19,4 +19,4 @@
 goals_limit := 1;
 
 loadpath := "IOA/meta_theory" :: "IOA/example" :: !loadpath;
-use_thy "Correctness"  handle _ => exit 1;
+use_thy "Correctness";
diff -r b86042000035 -r 23190112d369 src/HOL/Integ/ROOT.ML
--- a/src/HOL/Integ/ROOT.ML	Mon Apr 10 08:40:58 1995 +0200
+++ b/src/HOL/Integ/ROOT.ML	Mon Apr 10 08:47:43 1995 +0200
@@ -9,4 +9,4 @@
 CHOL_build_completed;    (*Cause examples to fail if CHOL did*)
 
 loadpath := ["Integ"];
-time_use_thy "Integ" handle _ => exit 1;
+time_use_thy "Integ";