tuned setup;

--- a/src/FOL/FOL.thy	Wed Apr 29 11:29:00 1998 +0200
+++ b/src/FOL/FOL.thy	Wed Apr 29 11:29:39 1998 +0200
@@ -4,6 +4,7 @@
 rules
   classical "(~P ==> P) ==> P"
 
-end
+setup
+  ClasetThyData.setup
 
-ML val thy_setup = [ClasetThyData.setup];
+end

--- a/src/FOL/IFOL.thy	Wed Apr 29 11:29:00 1998 +0200
+++ b/src/FOL/IFOL.thy	Wed Apr 29 11:29:39 1998 +0200
@@ -111,7 +111,8 @@
   eq_reflection   "(x=y)   ==> (x==y)"
   iff_reflection  "(P<->Q) ==> (P==Q)"
 
-end
 
+setup
+  Simplifier.setup
 
-ML val thy_setup = [Simplifier.setup];
+end

--- a/src/Provers/classical.ML	Wed Apr 29 11:29:00 1998 +0200
+++ b/src/Provers/classical.ML	Wed Apr 29 11:29:39 1998 +0200
@@ -28,7 +28,7 @@
 sig
   val clasetK: string
   exception ClasetData of object ref
-  val setup: theory -> theory
+  val setup: (theory -> theory) list
   val fix_methods: object * (object -> object) *
     (object * object -> object) * (Sign.sg -> object -> unit) -> unit
 end;
@@ -155,7 +155,7 @@
   fun merge exn = ! merge_fn exn;
   fun print sg exn = ! print_fn sg exn;
 in
-  val setup = Theory.init_data [(clasetK, (empty, prep_ext, merge, print))];
+  val setup = [Theory.init_data [(clasetK, (empty, prep_ext, merge, print))]];
   fun fix_methods (e, ext, mrg, prt) =
     (empty_ref := e; prep_ext_fn := ext; merge_fn := mrg; print_fn := prt);
 end;