removed 'old_datatype' command
authorblanchet
Tue Jan 02 16:11:20 2018 +0100 (21 months ago)
changeset 673180ee38196509e
parent 67317 15ea49331fc7
child 67319 07176d5b81d5
removed 'old_datatype' command
src/HOL/Library/Old_Datatype.thy
src/HOL/Tools/Old_Datatype/old_datatype.ML
     1.1 --- a/src/HOL/Library/Old_Datatype.thy	Tue Jan 02 16:08:59 2018 +0100
     1.2 +++ b/src/HOL/Library/Old_Datatype.thy	Tue Jan 02 16:11:20 2018 +0100
     1.3 @@ -7,10 +7,10 @@
     1.4  
     1.5  theory Old_Datatype
     1.6  imports Main
     1.7 -keywords "old_datatype" :: thy_decl
     1.8  begin
     1.9  
    1.10  ML_file "~~/src/HOL/Tools/datatype_realizer.ML"
    1.11 +ML_file "~~/src/HOL/Tools/inductive_realizer.ML"
    1.12  
    1.13  
    1.14  subsection \<open>The datatype universe\<close>
    1.15 @@ -512,6 +512,5 @@
    1.16  hide_const (open) Push Node Atom Leaf Numb Lim Split Case
    1.17  
    1.18  ML_file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML"
    1.19 -ML_file "~~/src/HOL/Tools/inductive_realizer.ML"
    1.20  
    1.21  end
     2.1 --- a/src/HOL/Tools/Old_Datatype/old_datatype.ML	Tue Jan 02 16:08:59 2018 +0100
     2.2 +++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML	Tue Jan 02 16:11:20 2018 +0100
     2.3 @@ -794,19 +794,6 @@
     2.4  val add_datatype = gen_add_datatype check_specs;
     2.5  val add_datatype_cmd = gen_add_datatype read_specs;
     2.6  
     2.7 -
     2.8 -(* outer syntax *)
     2.9 -
    2.10 -val spec_cmd =
    2.11 -  Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix --
    2.12 -  (@{keyword "="} |-- Parse.enum1 "|" (Parse.binding -- Scan.repeat Parse.typ -- Parse.opt_mixfix))
    2.13 -  >> (fn (((vs, t), mx), cons) => ((t, vs, mx), map Scan.triple1 cons));
    2.14 -
    2.15 -val _ =
    2.16 -  Outer_Syntax.command @{command_keyword old_datatype} "define old-style inductive datatypes"
    2.17 -    (Parse.and_list1 spec_cmd
    2.18 -      >> (Toplevel.theory o (snd oo add_datatype_cmd Old_Datatype_Aux.default_config)));
    2.19 -
    2.20  open Old_Datatype_Aux;
    2.21  
    2.22  end;