# HG changeset patch
# User blanchet
# Date 1514905880 -3600
# Node ID 0ee38196509ece137664184c9ae1b1d1ed0ce3e2
# Parent  15ea49331fc7441c8c05094131e3981549a413c0
removed 'old_datatype' command

diff -r 15ea49331fc7 -r 0ee38196509e src/HOL/Library/Old_Datatype.thy
--- a/src/HOL/Library/Old_Datatype.thy	Tue Jan 02 16:08:59 2018 +0100
+++ b/src/HOL/Library/Old_Datatype.thy	Tue Jan 02 16:11:20 2018 +0100
@@ -7,10 +7,10 @@
 
 theory Old_Datatype
 imports Main
-keywords "old_datatype" :: thy_decl
 begin
 
 ML_file "~~/src/HOL/Tools/datatype_realizer.ML"
+ML_file "~~/src/HOL/Tools/inductive_realizer.ML"
 
 
 subsection \<open>The datatype universe\<close>
@@ -512,6 +512,5 @@
 hide_const (open) Push Node Atom Leaf Numb Lim Split Case
 
 ML_file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"
-ML_file "~~/src/HOL/Tools/inductive_realizer.ML"
 
 end
diff -r 15ea49331fc7 -r 0ee38196509e src/HOL/Tools/Old_Datatype/old_datatype.ML
--- a/src/HOL/Tools/Old_Datatype/old_datatype.ML	Tue Jan 02 16:08:59 2018 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML	Tue Jan 02 16:11:20 2018 +0100
@@ -794,19 +794,6 @@
 val add_datatype = gen_add_datatype check_specs;
 val add_datatype_cmd = gen_add_datatype read_specs;
 
-
-(* outer syntax *)
-
-val spec_cmd =
-  Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix --
-  (@{keyword "="} |-- Parse.enum1 "|" (Parse.binding -- Scan.repeat Parse.typ -- Parse.opt_mixfix))
-  >> (fn (((vs, t), mx), cons) => ((t, vs, mx), map Scan.triple1 cons));
-
-val _ =
-  Outer_Syntax.command @{command_keyword old_datatype} "define old-style inductive datatypes"
-    (Parse.and_list1 spec_cmd
-      >> (Toplevel.theory o (snd oo add_datatype_cmd Old_Datatype_Aux.default_config)));
-
 open Old_Datatype_Aux;
 
 end;