# HG changeset patch
# User wenzelm
# Date 891683056 -7200
# Node ID 0cc16c8133bb8590dfa3a4998c220df41752bf5d
# Parent  5adb93457e3956dd1d00855b47ecc5c02bf8fb3e
replaced thy_data by setup;

diff -r 5adb93457e39 -r 0cc16c8133bb src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sat Apr 04 11:43:39 1998 +0200
+++ b/src/Provers/classical.ML	Sat Apr 04 11:44:16 1998 +0200
@@ -28,8 +28,7 @@
 sig
   val clasetK: string
   exception ClasetData of object ref
-  val thy_data: string * (object * (object -> object) *
-    (object * object -> object) * (Sign.sg -> object -> unit))
+  val setup: theory -> theory
   val fix_methods: object * (object -> object) *
     (object * object -> object) * (Sign.sg -> object -> unit) -> unit
 end;
@@ -156,7 +155,7 @@
   fun merge exn = ! merge_fn exn;
   fun print sg exn = ! print_fn sg exn;
 in
-  val thy_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;