diff -r 8cd051d5cf74 -r 811481779743 Integ/ROOT.ML --- a/Integ/ROOT.ML Thu Apr 06 11:32:47 1995 +0200 +++ b/Integ/ROOT.ML Thu Apr 06 11:35:33 1995 +0200 @@ -9,4 +9,4 @@ HOL_build_completed; (*Cause examples to fail if HOL did*) loadpath := ["Integ"]; -time_use_thy "Integ" handle _ => exit 1; +time_use_thy "Integ";