diff -r 0ccba1b6d00b -r a09ec6daaa19 src/HOL/BNF_Examples/SML.thy
--- a/src/HOL/BNF_Examples/SML.thy	Thu Sep 11 19:20:23 2014 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,91 +0,0 @@
-(*  Title:      HOL/Datatype_Benchmark/SML.thy
-
-Example from Myra: part of the syntax of SML.
-*)
-
-theory SML imports Main begin
-
-datatype
-  string = EMPTY_STRING | CONS_STRING nat string
-
-datatype
-   strid = STRID string
-
-datatype
-   var = VAR string
-
-datatype
-   con = CON string
-
-datatype
-   scon = SCINT nat | SCSTR string
-
-datatype
-   excon = EXCON string
-
-datatype
-   label = LABEL string
-
-datatype
-  'a nonemptylist = Head_and_tail 'a "'a list"
-
-datatype
-  '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"
-           | PARatpat_e pat_e
-and
-   patrow_e = DOTDOTDOT_e
-            | 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
-         | LAYEREDpat_e var pat_e
-and
-   conbind_e = CONBIND_e con "conbind_e option"
-and
-   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"
-and
-   atexp_e = SCONatexp_e scon
-           | 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"
-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"
-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"
-         | EMPTYdec_e
-         | SEQdec_e dec_e dec_e
-and
-   valbind_e = PLAINvalbind_e pat_e exp_e "valbind_e option"
-             | RECvalbind_e valbind_e
-
-end