# HG changeset patch
# User wenzelm
# Date 891685719 -7200
# Node ID 03fd006fb97ba6889ae838bab64143c16e3fced2
# Parent  8e3c2dddb9c8b2186888e7e3263c3d77aee17f8a
replaced thy_data by thy_setup;

diff -r 8e3c2dddb9c8 -r 03fd006fb97b src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Sat Apr 04 12:26:47 1998 +0200
+++ b/src/FOL/FOL.thy	Sat Apr 04 12:28:39 1998 +0200
@@ -6,4 +6,4 @@
 
 end
 
-ML val thy_data = [ClasetThyData.thy_data];
+ML val thy_setup = [ClasetThyData.setup];
diff -r 8e3c2dddb9c8 -r 03fd006fb97b src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Sat Apr 04 12:26:47 1998 +0200
+++ b/src/FOL/IFOL.thy	Sat Apr 04 12:28:39 1998 +0200
@@ -114,4 +114,4 @@
 end
 
 
-ML val thy_data = [Simplifier.simpset_thy_data];
+ML val thy_setup = [Simplifier.setup];
diff -r 8e3c2dddb9c8 -r 03fd006fb97b src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sat Apr 04 12:26:47 1998 +0200
+++ b/src/HOL/HOL.thy	Sat Apr 04 12:28:39 1998 +0200
@@ -191,6 +191,12 @@
 
 ML
 
+
+(** initial HOL theory setup **)
+
+val thy_setup = [Simplifier.setup, ClasetThyData.setup, ThyData.setup];
+
+
 (** Choice between the HOL and Isabelle style of quantifiers **)
 
 val HOL_quantifiers = ref true;
@@ -207,8 +213,3 @@
 
 val print_ast_translation =
   map alt_ast_tr' [("! ", "*All"), ("? ", "*Ex"), ("?! ", "*Ex1")];
-
-
-(** HOL theory data **)
-
-val thy_data = ThyData.hol_data;