src/ZF/Datatype_ZF.thy
changeset 26480 544cef16045b
parent 26056 6a0801279f4c
child 26928 ca87aff1ad2d
     1.1 --- a/src/ZF/Datatype_ZF.thy	Sat Mar 29 19:13:58 2008 +0100
     1.2 +++ b/src/ZF/Datatype_ZF.thy	Sat Mar 29 19:14:00 2008 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4  uses "Tools/datatype_package.ML"
     1.5  begin
     1.6  
     1.7 -ML_setup {*
     1.8 +ML {*
     1.9  (*Typechecking rules for most datatypes involving univ*)
    1.10  structure Data_Arg =
    1.11    struct