1.1 --- a/src/HOL/HOL.thy	Wed Apr 29 11:40:37 1998 +0200
     1.2 +++ b/src/HOL/HOL.thy	Wed Apr 29 11:41:08 1998 +0200
     1.3 @@ -77,7 +77,7 @@
     1.4  
     1.5  (** Additional concrete syntax **)
     1.6  
     1.7 -types
     1.8 +nonterminals
     1.9    letbinds  letbind
    1.10    case_syn  cases_syn
    1.11  
    1.12 @@ -186,15 +186,18 @@
    1.13    arbitrary_def "False ==> arbitrary == (@x. False)"
    1.14  
    1.15  
    1.16 -end
    1.17 -
    1.18 -
    1.19 -ML
    1.20 -
    1.21  
    1.22  (** initial HOL theory setup **)
    1.23  
    1.24 -val thy_setup = [Simplifier.setup, ClasetThyData.setup, ThyData.setup];
    1.25 +setup Simplifier.setup
    1.26 +setup ClasetThyData.setup
    1.27 +setup ThyData.setup
    1.28 +
    1.29 +
    1.30 +end
    1.31 +
    1.32 +
    1.33 +ML
    1.34  
    1.35  
    1.36  (** Choice between the HOL and Isabelle style of quantifiers **)