killed temporary "data_raw" and "codata_raw" now that the examples have been ported to "data" and "codata"
authorblanchet
Fri Sep 28 09:12:50 2012 +0200 (2012-09-28)
changeset 49635fc0777f04205
parent 49634 9a21861a2d5c
child 49636 b7256a88a84b
killed temporary "data_raw" and "codata_raw" now that the examples have been ported to "data" and "codata"
etc/isar-keywords.el
src/HOL/BNF/BNF_GFP.thy
src/HOL/BNF/BNF_LFP.thy
src/HOL/BNF/Tools/bnf_fp.ML
src/HOL/BNF/Tools/bnf_gfp.ML
src/HOL/BNF/Tools/bnf_lfp.ML
     1.1 --- a/etc/isar-keywords.el	Fri Sep 28 09:12:50 2012 +0200
     1.2 +++ b/etc/isar-keywords.el	Fri Sep 28 09:12:50 2012 +0200
     1.3 @@ -48,7 +48,6 @@
     1.4      "classes"
     1.5      "classrel"
     1.6      "codata"
     1.7 -    "codata_raw"
     1.8      "code_abort"
     1.9      "code_class"
    1.10      "code_const"
    1.11 @@ -71,7 +70,6 @@
    1.12      "corollary"
    1.13      "cpodef"
    1.14      "data"
    1.15 -    "data_raw"
    1.16      "datatype"
    1.17      "declaration"
    1.18      "declare"
    1.19 @@ -483,7 +481,6 @@
    1.20      "classes"
    1.21      "classrel"
    1.22      "codata"
    1.23 -    "codata_raw"
    1.24      "code_abort"
    1.25      "code_class"
    1.26      "code_const"
    1.27 @@ -500,7 +497,6 @@
    1.28      "consts"
    1.29      "context"
    1.30      "data"
    1.31 -    "data_raw"
    1.32      "datatype"
    1.33      "declaration"
    1.34      "declare"
     2.1 --- a/src/HOL/BNF/BNF_GFP.thy	Fri Sep 28 09:12:50 2012 +0200
     2.2 +++ b/src/HOL/BNF/BNF_GFP.thy	Fri Sep 28 09:12:50 2012 +0200
     2.3 @@ -10,7 +10,6 @@
     2.4  theory BNF_GFP
     2.5  imports BNF_FP Equiv_Relations_More "~~/src/HOL/Library/Prefix_Order"
     2.6  keywords
     2.7 -  "codata_raw" :: thy_decl and
     2.8    "codata" :: thy_decl
     2.9  begin
    2.10  
     3.1 --- a/src/HOL/BNF/BNF_LFP.thy	Fri Sep 28 09:12:50 2012 +0200
     3.2 +++ b/src/HOL/BNF/BNF_LFP.thy	Fri Sep 28 09:12:50 2012 +0200
     3.3 @@ -10,7 +10,6 @@
     3.4  theory BNF_LFP
     3.5  imports BNF_FP
     3.6  keywords
     3.7 -  "data_raw" :: thy_decl and
     3.8    "data" :: thy_decl
     3.9  begin
    3.10  
     4.1 --- a/src/HOL/BNF/Tools/bnf_fp.ML	Fri Sep 28 09:12:50 2012 +0200
     4.2 +++ b/src/HOL/BNF/Tools/bnf_fp.ML	Fri Sep 28 09:12:50 2012 +0200
     4.3 @@ -144,9 +144,6 @@
     4.4      typ list * typ list list -> BNF_Def.BNF list -> local_theory -> 'a) ->
     4.5      binding list -> mixfix list -> (string * sort) list -> ((string * sort) * typ) list ->
     4.6      local_theory -> BNF_Def.BNF list * 'a
     4.7 -  val fp_bnf_cmd: (mixfix list -> (string * sort) list option -> binding list ->
     4.8 -    typ list * typ list list -> BNF_Def.BNF list -> local_theory -> 'a) ->
     4.9 -    binding list * (string list * string list) -> local_theory -> 'a
    4.10  end;
    4.11  
    4.12  structure BNF_FP : BNF_FP =
    4.13 @@ -437,19 +434,4 @@
    4.14      mk_fp_bnf timer (construct_fp mixfixes) (SOME resBs) bs sort lhss bnfs Dss Ass unfold_set lthy'
    4.15    end;
    4.16  
    4.17 -fun fp_bnf_cmd construct_fp (bs, (raw_lhss, raw_bnfs)) lthy =
    4.18 -  let
    4.19 -    val timer = time (Timer.startRealTimer ());
    4.20 -    val lhss = map (dest_TFree o Syntax.read_typ lthy) raw_lhss;
    4.21 -    val sort = fp_sort lhss NONE;
    4.22 -    fun qualify b = Binding.qualify true (Binding.name_of (Binding.prefix_name rawN b));
    4.23 -    val ((bnfs, (Dss, Ass)), (unfold_set, lthy')) = apfst (apsnd split_list o split_list)
    4.24 -      (fold_map2 (fn b => fn rawT =>
    4.25 -        (bnf_of_typ Smart_Inline (qualify b) sort (Syntax.read_typ lthy rawT)))
    4.26 -      bs raw_bnfs (empty_unfolds, lthy));
    4.27 -  in
    4.28 -    snd (mk_fp_bnf timer
    4.29 -      (construct_fp (map (K NoSyn) bs)) NONE bs sort lhss bnfs Dss Ass unfold_set lthy')
    4.30 -  end;
    4.31 -
    4.32  end;
     5.1 --- a/src/HOL/BNF/Tools/bnf_gfp.ML	Fri Sep 28 09:12:50 2012 +0200
     5.2 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Fri Sep 28 09:12:50 2012 +0200
     5.3 @@ -3004,13 +3004,6 @@
     5.4    end;
     5.5  
     5.6  val _ =
     5.7 -  Outer_Syntax.local_theory @{command_spec "codata_raw"}
     5.8 -    "define BNF-based coinductive datatypes (low-level)"
     5.9 -    (Parse.and_list1
    5.10 -      ((Parse.binding --| @{keyword ":"}) -- (Parse.typ --| @{keyword "="} -- Parse.typ)) >>
    5.11 -      (snd oo fp_bnf_cmd construct_gfp o apsnd split_list o split_list));
    5.12 -
    5.13 -val _ =
    5.14    Outer_Syntax.local_theory @{command_spec "codata"} "define BNF-based coinductive datatypes"
    5.15      (parse_datatype_cmd false construct_gfp);
    5.16  
     6.1 --- a/src/HOL/BNF/Tools/bnf_lfp.ML	Fri Sep 28 09:12:50 2012 +0200
     6.2 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Fri Sep 28 09:12:50 2012 +0200
     6.3 @@ -1835,13 +1835,6 @@
     6.4    end;
     6.5  
     6.6  val _ =
     6.7 -  Outer_Syntax.local_theory @{command_spec "data_raw"}
     6.8 -    "define BNF-based inductive datatypes (low-level)"
     6.9 -    (Parse.and_list1
    6.10 -      ((Parse.binding --| @{keyword ":"}) -- (Parse.typ --| @{keyword "="} -- Parse.typ)) >>
    6.11 -      (snd oo fp_bnf_cmd construct_lfp o apsnd split_list o split_list));
    6.12 -
    6.13 -val _ =
    6.14    Outer_Syntax.local_theory @{command_spec "data"} "define BNF-based inductive datatypes"
    6.15      (parse_datatype_cmd true construct_lfp);
    6.16