replaced thy_data by thy_setup;
authorwenzelm
Sat, 04 Apr 1998 12:28:39 +0200
changeset 4793 03fd006fb97b
parent 4792 8e3c2dddb9c8
child 4794 9db0916ecdae
replaced thy_data by thy_setup;
src/FOL/FOL.thy
src/FOL/IFOL.thy
src/HOL/HOL.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];
--- 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;