--- 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
--- 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;