src/ZF/Tools/datatype_package.ML
changeset 24867 e5b55d7be9bb
parent 24826 78e6a3cea367
child 24893 b8ef7afe3a6b
     1.1 --- a/src/ZF/Tools/datatype_package.ML	Sat Oct 06 16:41:22 2007 +0200
     1.2 +++ b/src/ZF/Tools/datatype_package.ML	Sat Oct 06 16:50:04 2007 +0200
     1.3 @@ -422,11 +422,9 @@
     1.4  
     1.5  val coind_prefix = if coind then "co" else "";
     1.6  
     1.7 -val inductiveP = OuterSyntax.command (coind_prefix ^ "datatype")
     1.8 +val _ = OuterSyntax.command (coind_prefix ^ "datatype")
     1.9    ("define " ^ coind_prefix ^ "datatype") K.thy_decl datatype_decl;
    1.10  
    1.11 -val _ = OuterSyntax.add_parsers [inductiveP];
    1.12 -
    1.13  end;
    1.14  
    1.15  end;