# HG changeset patch
# User wenzelm
# Date 893842868 -7200
# Node ID 843a9f5b3c3d2722fb67cab800eec83a0219b98f
# Parent  9be2bf0ce90951b931b8953af9e2aec85984c45b
nonterminals;
tuned setup;

diff -r 9be2bf0ce909 -r 843a9f5b3c3d src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Apr 29 11:40:37 1998 +0200
+++ b/src/HOL/HOL.thy	Wed Apr 29 11:41:08 1998 +0200
@@ -77,7 +77,7 @@
 
 (** Additional concrete syntax **)
 
-types
+nonterminals
   letbinds  letbind
   case_syn  cases_syn
 
@@ -186,17 +186,20 @@
   arbitrary_def "False ==> arbitrary == (@x. False)"
 
 
+
+(** initial HOL theory setup **)
+
+setup Simplifier.setup
+setup ClasetThyData.setup
+setup ThyData.setup
+
+
 end
 
 
 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;