# HG changeset patch
# User nipkow
# Date 797496540 -7200
# Node ID f2dc38ed53ac6fab0e9810490b8c8efa099dd9ca
# Parent  23190112d369ce38621517e4781a049d15771f12
ROOT.ML: Removed the "exit 1" calls, since now the Makefile does them.
MT.thy: Deleted extra space in clos_mk.

diff -r 23190112d369 -r f2dc38ed53ac src/HOL/ex/MT.thy
--- a/src/HOL/ex/MT.thy	Mon Apr 10 08:47:43 1995 +0200
+++ b/src/HOL/ex/MT.thy	Mon Apr 10 08:49:00 1995 +0200
@@ -66,7 +66,7 @@
   ve_dom :: "ValEnv => ExVar set"
   ve_app :: "[ValEnv, ExVar] => Val"
 
-  clos_mk :: "[ExVar, Ex, ValEnv] => Clos" ("<| _  , _ , _ |>" [0,0,0] 1000)
+  clos_mk :: "[ExVar, Ex, ValEnv] => Clos" ("<| _ , _ , _ |>" [0,0,0] 1000)
 
   te_emp :: "TyEnv"
   te_owr :: "[TyEnv, ExVar, Ty] => TyEnv" ("_ + { _ |=> _ }" [36,0,0] 50)
diff -r 23190112d369 -r f2dc38ed53ac src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Mon Apr 10 08:47:43 1995 +0200
+++ b/src/HOL/ex/ROOT.ML	Mon Apr 10 08:49:00 1995 +0200
@@ -8,25 +8,24 @@
 
 CHOL_build_completed;    (*Cause examples to fail if CHOL did*)
 
-(writeln "Root file for CHOL examples";
- proof_timing := true;
- loadpath := ["ex"];
- time_use     "ex/cla.ML";
- time_use     "ex/meson.ML";
- time_use     "ex/mesontest.ML";
- time_use_thy "String";
- time_use_thy "InSort";
- time_use_thy "Qsort";
- time_use_thy "LexProd";
- time_use_thy "Puzzle";
- time_use_thy "NatSum";
- time_use     "ex/set.ML";
- time_use_thy "SList";
- time_use_thy "LList";
- time_use_thy "Acc";
- time_use_thy "PropLog";
- time_use_thy "Term";
- time_use_thy "Simult";
- time_use_thy "MT";
- writeln "END: Root file for CHOL examples"
-)  handle _ => exit 1;
+writeln "Root file for CHOL examples";
+proof_timing := true;
+loadpath := ["ex"];
+time_use     "ex/cla.ML";
+time_use     "ex/meson.ML";
+time_use     "ex/mesontest.ML";
+time_use_thy "String";
+time_use_thy "InSort";
+time_use_thy "Qsort";
+time_use_thy "LexProd";
+time_use_thy "Puzzle";
+time_use_thy "NatSum";
+time_use     "ex/set.ML";
+time_use_thy "SList";
+time_use_thy "LList";
+time_use_thy "Acc";
+time_use_thy "PropLog";
+time_use_thy "Term";
+time_use_thy "Simult";
+time_use_thy "MT";
+writeln "END: Root file for CHOL examples";