# HG changeset patch
# User lcp
# Date 797160474 -7200
# Node ID b67c8e01ae046522080984ceb6df3a4ada7b5715
# Parent  2209eb5bb56b00de15926f3d8d945f057063882d
Removed the "exit 1" calls, since now the
Makefile does them.

diff -r 2209eb5bb56b -r b67c8e01ae04 IMP/ROOT.ML
--- a/IMP/ROOT.ML	Thu Apr 06 11:24:11 1995 +0200
+++ b/IMP/ROOT.ML	Thu Apr 06 11:27:54 1995 +0200
@@ -17,6 +17,5 @@
 writeln"Root file for HOL/IMP";
 proof_timing := true;
 loadpath := [".","IMP"];
-(time_use_thy "Properties";
- time_use_thy "Equiv"
-)  handle _ => exit 1;
+time_use_thy "Properties";
+time_use_thy "Equiv";
diff -r 2209eb5bb56b -r b67c8e01ae04 IOA/ROOT.ML
--- a/IOA/ROOT.ML	Thu Apr 06 11:24:11 1995 +0200
+++ b/IOA/ROOT.ML	Thu Apr 06 11:27:54 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";