# HG changeset patch
# User blanchet
# Date 1348816370 -7200
# Node ID fc0777f0420548afa0f2c1f60c1ae2b7565e4c1c
# Parent  9a21861a2d5caa3a4d0468b394bd141e1daf07fc
killed temporary "data_raw" and "codata_raw" now that the examples have been ported to "data" and "codata"

diff -r 9a21861a2d5c -r fc0777f04205 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Fri Sep 28 09:12:50 2012 +0200
+++ b/etc/isar-keywords.el	Fri Sep 28 09:12:50 2012 +0200
@@ -48,7 +48,6 @@
     "classes"
     "classrel"
     "codata"
-    "codata_raw"
     "code_abort"
     "code_class"
     "code_const"
@@ -71,7 +70,6 @@
     "corollary"
     "cpodef"
     "data"
-    "data_raw"
     "datatype"
     "declaration"
     "declare"
@@ -483,7 +481,6 @@
     "classes"
     "classrel"
     "codata"
-    "codata_raw"
     "code_abort"
     "code_class"
     "code_const"
@@ -500,7 +497,6 @@
     "consts"
     "context"
     "data"
-    "data_raw"
     "datatype"
     "declaration"
     "declare"
diff -r 9a21861a2d5c -r fc0777f04205 src/HOL/BNF/BNF_GFP.thy
--- a/src/HOL/BNF/BNF_GFP.thy	Fri Sep 28 09:12:50 2012 +0200
+++ b/src/HOL/BNF/BNF_GFP.thy	Fri Sep 28 09:12:50 2012 +0200
@@ -10,7 +10,6 @@
 theory BNF_GFP
 imports BNF_FP Equiv_Relations_More "~~/src/HOL/Library/Prefix_Order"
 keywords
-  "codata_raw" :: thy_decl and
   "codata" :: thy_decl
 begin
 
diff -r 9a21861a2d5c -r fc0777f04205 src/HOL/BNF/BNF_LFP.thy
--- a/src/HOL/BNF/BNF_LFP.thy	Fri Sep 28 09:12:50 2012 +0200
+++ b/src/HOL/BNF/BNF_LFP.thy	Fri Sep 28 09:12:50 2012 +0200
@@ -10,7 +10,6 @@
 theory BNF_LFP
 imports BNF_FP
 keywords
-  "data_raw" :: thy_decl and
   "data" :: thy_decl
 begin
 
diff -r 9a21861a2d5c -r fc0777f04205 src/HOL/BNF/Tools/bnf_fp.ML
--- a/src/HOL/BNF/Tools/bnf_fp.ML	Fri Sep 28 09:12:50 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp.ML	Fri Sep 28 09:12:50 2012 +0200
@@ -144,9 +144,6 @@
     typ list * typ list list -> BNF_Def.BNF list -> local_theory -> 'a) ->
     binding list -> mixfix list -> (string * sort) list -> ((string * sort) * typ) list ->
     local_theory -> BNF_Def.BNF list * 'a
-  val fp_bnf_cmd: (mixfix list -> (string * sort) list option -> binding list ->
-    typ list * typ list list -> BNF_Def.BNF list -> local_theory -> 'a) ->
-    binding list * (string list * string list) -> local_theory -> 'a
 end;
 
 structure BNF_FP : BNF_FP =
@@ -437,19 +434,4 @@
     mk_fp_bnf timer (construct_fp mixfixes) (SOME resBs) bs sort lhss bnfs Dss Ass unfold_set lthy'
   end;
 
-fun fp_bnf_cmd construct_fp (bs, (raw_lhss, raw_bnfs)) lthy =
-  let
-    val timer = time (Timer.startRealTimer ());
-    val lhss = map (dest_TFree o Syntax.read_typ lthy) raw_lhss;
-    val sort = fp_sort lhss NONE;
-    fun qualify b = Binding.qualify true (Binding.name_of (Binding.prefix_name rawN b));
-    val ((bnfs, (Dss, Ass)), (unfold_set, lthy')) = apfst (apsnd split_list o split_list)
-      (fold_map2 (fn b => fn rawT =>
-        (bnf_of_typ Smart_Inline (qualify b) sort (Syntax.read_typ lthy rawT)))
-      bs raw_bnfs (empty_unfolds, lthy));
-  in
-    snd (mk_fp_bnf timer
-      (construct_fp (map (K NoSyn) bs)) NONE bs sort lhss bnfs Dss Ass unfold_set lthy')
-  end;
-
 end;
diff -r 9a21861a2d5c -r fc0777f04205 src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Fri Sep 28 09:12:50 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Fri Sep 28 09:12:50 2012 +0200
@@ -3004,13 +3004,6 @@
   end;
 
 val _ =
-  Outer_Syntax.local_theory @{command_spec "codata_raw"}
-    "define BNF-based coinductive datatypes (low-level)"
-    (Parse.and_list1
-      ((Parse.binding --| @{keyword ":"}) -- (Parse.typ --| @{keyword "="} -- Parse.typ)) >>
-      (snd oo fp_bnf_cmd construct_gfp o apsnd split_list o split_list));
-
-val _ =
   Outer_Syntax.local_theory @{command_spec "codata"} "define BNF-based coinductive datatypes"
     (parse_datatype_cmd false construct_gfp);
 
diff -r 9a21861a2d5c -r fc0777f04205 src/HOL/BNF/Tools/bnf_lfp.ML
--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Fri Sep 28 09:12:50 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Fri Sep 28 09:12:50 2012 +0200
@@ -1835,13 +1835,6 @@
   end;
 
 val _ =
-  Outer_Syntax.local_theory @{command_spec "data_raw"}
-    "define BNF-based inductive datatypes (low-level)"
-    (Parse.and_list1
-      ((Parse.binding --| @{keyword ":"}) -- (Parse.typ --| @{keyword "="} -- Parse.typ)) >>
-      (snd oo fp_bnf_cmd construct_lfp o apsnd split_list o split_list));
-
-val _ =
   Outer_Syntax.local_theory @{command_spec "data"} "define BNF-based inductive datatypes"
     (parse_datatype_cmd true construct_lfp);