--- 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];
--- 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];
--- 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;