Admin/Benchmarks/HOL-datatype/SML.thy

 (*  Title:      Admin/Benchmarks/HOL-datatype/SML.thy
     ID:         $Id$
 *)
 
-SML = Main +
+theory SML = Main:
 
 (* ------------------------------------------------------------------------- *)
 (* Example from Myra: part of the syntax of SML.                             *)
 (* ------------------------------------------------------------------------- *)
 

 
 datatype
    label = LABEL string
 
 datatype
-  'a nonemptylist = Head_and_tail 'a ('a list)
+  'a nonemptylist = Head_and_tail 'a "'a list"
 
 datatype
-  'a long = BASE 'a | QUALIFIED strid ('a long)
+  'a long = BASE 'a | QUALIFIED strid "'a long"
 
 datatype
    atpat_e = WILDCARDatpat_e
            | SCONatpat_e scon
            | VARatpat_e var
-           | CONatpat_e (con long)
-           | EXCONatpat_e (excon long)
-           | RECORDatpat_e (patrow_e option)
+           | CONatpat_e "con long"
+           | EXCONatpat_e "excon long"
+           | RECORDatpat_e "patrow_e option"
            | PARatpat_e pat_e
 and
    patrow_e = DOTDOTDOT_e
-            | PATROW_e label pat_e (patrow_e option)
+            | PATROW_e label pat_e "patrow_e option"
 and
    pat_e = ATPATpat_e atpat_e
-         | CONpat_e (con long) atpat_e
-         | EXCONpat_e (excon long) atpat_e
+         | CONpat_e "con long" atpat_e
+         | EXCONpat_e "excon long" atpat_e
          | LAYEREDpat_e var pat_e
 and
-   conbind_e = CONBIND_e con (conbind_e option)
+   conbind_e = CONBIND_e con "conbind_e option"
 and
-   datbind_e = DATBIND_e conbind_e (datbind_e option)
+   datbind_e = DATBIND_e conbind_e "datbind_e option"
 and
-   exbind_e = EXBIND1_e excon (exbind_e option)
-            | EXBIND2_e excon (excon long) (exbind_e option)
+   exbind_e = EXBIND1_e excon "exbind_e option"
+            | EXBIND2_e excon "excon long" "exbind_e option"
 and
    atexp_e = SCONatexp_e scon
-           | VARatexp_e (var long)
-           | CONatexp_e (con long)
-           | EXCONatexp_e (excon long)
-           | RECORDatexp_e (exprow_e option)
+           | VARatexp_e "var long"
+           | CONatexp_e "con long"
+           | EXCONatexp_e "excon long"
+           | RECORDatexp_e "exprow_e option"
            | LETatexp_e dec_e exp_e
            | PARatexp_e exp_e
 and
-   exprow_e = EXPROW_e label exp_e (exprow_e option)
+   exprow_e = EXPROW_e label exp_e "exprow_e option"
 and
    exp_e = ATEXPexp_e atexp_e
          | APPexp_e exp_e atexp_e
          | HANDLEexp_e exp_e match_e
          | RAISEexp_e exp_e
          | FNexp_e match_e
 and
-   match_e = MATCH_e mrule_e (match_e option)
+   match_e = MATCH_e mrule_e "match_e option"
 and
    mrule_e = MRULE_e pat_e exp_e
 and
    dec_e = VALdec_e valbind_e
          | DATATYPEdec_e datbind_e
          | ABSTYPEdec_e datbind_e dec_e
          | EXCEPTdec_e exbind_e
          | LOCALdec_e dec_e dec_e
-         | OPENdec_e ((strid long) nonemptylist)
+         | OPENdec_e "strid long nonemptylist"
          | EMPTYdec_e
          | SEQdec_e dec_e dec_e
 and
-   valbind_e = PLAINvalbind_e pat_e exp_e (valbind_e option)
+   valbind_e = PLAINvalbind_e pat_e exp_e "valbind_e option"
              | RECvalbind_e valbind_e
 
 end