proper use of ioa_package.ML;

--- a/src/HOLCF/IOA/ROOT.ML	Tue Jul 03 22:27:25 2007 +0200
+++ b/src/HOLCF/IOA/ROOT.ML	Tue Jul 03 22:27:27 2007 +0200
@@ -2,11 +2,8 @@
     ID:         $Id$
     Author:     Olaf Mueller
 
-This is the ROOT file for the formalization of a semantic model of
-I/O-Automata.  See the README.html file for details.
+Formalization of a semantic model of I/O-Automata.  See README.html
+for details.
 *)
 
-goals_limit := 1;
-
 time_use_thy "meta_theory/Abstraction";
-time_use "meta_theory/ioa_package.ML";

--- a/src/HOLCF/IOA/meta_theory/Abstraction.thy	Tue Jul 03 22:27:25 2007 +0200
+++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy	Tue Jul 03 22:27:27 2007 +0200
@@ -7,6 +7,7 @@
 
 theory Abstraction
 imports LiveIOA
+uses ("ioa_package.ML")
 begin
 
 defaultsort type
@@ -639,4 +640,6 @@
 end
 *}
 
+use "ioa_package.ML"
+
 end