1.1 --- a/src/Tools/isac/MathEngBasic/MathEngBasic.thy	Tue Dec 17 16:33:24 2019 +0100
     1.2 +++ b/src/Tools/isac/MathEngBasic/MathEngBasic.thy	Tue Dec 17 16:35:29 2019 +0100
     1.3 @@ -21,32 +21,6 @@
     1.4  
     1.5  ML \<open>
     1.6  \<close> ML \<open>
     1.7 -signature XXX_DEF =
     1.8 -sig
     1.9 -  datatype xxx_def = Aaa of string | Bbb of string
    1.10 -end
    1.11 -\<close> ML \<open>
    1.12 -structure Xxx_Def: XXX_DEF(**) =
    1.13 -struct
    1.14 -  datatype xxx_def = Aaa of string | Bbb of string
    1.15 -end
    1.16 -\<close> ML \<open>
    1.17 -Xxx_Def.Aaa "works"
    1.18 -\<close> ML \<open>
    1.19 -\<close> ML \<open>
    1.20 -\<close> ML \<open>
    1.21 -signature XXX =
    1.22 -sig
    1.23 -  datatype xxx = Aaa of string | Bbb of string
    1.24 -end
    1.25 -\<close> ML \<open>
    1.26 -structure Xxx: XXX(**) =
    1.27 -struct
    1.28 -  open Xxx_Def
    1.29 -  datatype xxx = datatype xxx_def
    1.30 -end
    1.31 -\<close> ML \<open>
    1.32 -Xxx.Aaa "works"
    1.33  \<close> ML \<open>
    1.34  \<close>
    1.35  end