renamed BNF "(co)data" commands to names that are closer to their final names

--- a/etc/isar-keywords.el	Mon Apr 29 06:13:36 2013 +0200
+++ b/etc/isar-keywords.el	Mon Apr 29 09:10:49 2013 +0200
@@ -46,7 +46,7 @@
     "class_deps"
     "classes"
     "classrel"
-    "codata"
+    "codatatype"
     "code_abort"
     "code_class"
     "code_const"
@@ -68,8 +68,8 @@
     "context"
     "corollary"
     "cpodef"
-    "data"
     "datatype"
+    "datatype_new"
     "declaration"
     "declare"
     "def"
@@ -482,7 +482,7 @@
     "class"
     "classes"
     "classrel"
-    "codata"
+    "codatatype"
     "code_abort"
     "code_class"
     "code_const"
@@ -498,8 +498,8 @@
     "coinductive_set"
     "consts"
     "context"
-    "data"
     "datatype"
+    "datatype_new"
     "declaration"
     "declare"
     "default_sort"

--- a/src/HOL/BNF/BNF_GFP.thy	Mon Apr 29 06:13:36 2013 +0200
+++ b/src/HOL/BNF/BNF_GFP.thy	Mon Apr 29 09:10:49 2013 +0200
@@ -10,7 +10,7 @@
 theory BNF_GFP
 imports BNF_FP Equiv_Relations_More "~~/src/HOL/Library/Sublist"
 keywords
-  "codata" :: thy_decl
+  "codatatype" :: thy_decl
 begin
 
 lemma o_sum_case: "h o sum_case f g = sum_case (h o f) (h o g)"

--- a/src/HOL/BNF/BNF_LFP.thy	Mon Apr 29 06:13:36 2013 +0200
+++ b/src/HOL/BNF/BNF_LFP.thy	Mon Apr 29 09:10:49 2013 +0200
@@ -10,7 +10,7 @@
 theory BNF_LFP
 imports BNF_FP
 keywords
-  "data" :: thy_decl
+  "datatype_new" :: thy_decl
 begin
 
 lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}"

--- a/src/HOL/BNF/Examples/Derivation_Trees/DTree.thy	Mon Apr 29 06:13:36 2013 +0200
+++ b/src/HOL/BNF/Examples/Derivation_Trees/DTree.thy	Mon Apr 29 09:10:49 2013 +0200
@@ -16,7 +16,7 @@
 typedecl N
 typedecl T
 
-codata dtree = NNode (root: N) (ccont: "(T + dtree) fset")
+codatatype dtree = NNode (root: N) (ccont: "(T + dtree) fset")
 
 subsection{* Transporting the Characteristic Lemmas from @{text "fset"} to @{text "set"} *}
 

--- a/src/HOL/BNF/Examples/Lambda_Term.thy	Mon Apr 29 06:13:36 2013 +0200
+++ b/src/HOL/BNF/Examples/Lambda_Term.thy	Mon Apr 29 09:10:49 2013 +0200
@@ -15,7 +15,7 @@
 
 section {* Datatype definition *}
 
-data 'a trm =
+datatype_new 'a trm =
   Var 'a |
   App "'a trm" "'a trm" |
   Lam 'a "'a trm" |

--- a/src/HOL/BNF/Examples/ListF.thy	Mon Apr 29 06:13:36 2013 +0200
+++ b/src/HOL/BNF/Examples/ListF.thy	Mon Apr 29 09:10:49 2013 +0200
@@ -12,7 +12,7 @@
 imports "../BNF"
 begin
 
-data (rep_compat) 'a listF = NilF | Conss 'a "'a listF"
+datatype_new (rep_compat) 'a listF = NilF | Conss 'a "'a listF"
 
 lemma fold_sum_case_NilF: "listF_ctor_fold (sum_case f g) NilF = f ()"
 unfolding NilF_def listF.ctor_fold pre_listF_map_def by simp

--- a/src/HOL/BNF/Examples/Misc_Codata.thy	Mon Apr 29 06:13:36 2013 +0200
+++ b/src/HOL/BNF/Examples/Misc_Codata.thy	Mon Apr 29 09:10:49 2013 +0200
@@ -12,24 +12,24 @@
 imports "../BNF"
 begin
 
-codata simple = X1 | X2 | X3 | X4
+codatatype simple = X1 | X2 | X3 | X4
 
-codata simple' = X1' unit | X2' unit | X3' unit | X4' unit
+codatatype simple' = X1' unit | X2' unit | X3' unit | X4' unit
 
-codata 'a stream = Stream 'a "'a stream"
+codatatype 'a stream = Stream 'a "'a stream"
 
-codata 'a mylist = MyNil | MyCons 'a "'a mylist"
+codatatype 'a mylist = MyNil | MyCons 'a "'a mylist"
 
-codata ('b, 'c, 'd, 'e) some_passive =
+codatatype ('b, 'c, 'd, 'e) some_passive =
   SP1 "('b, 'c, 'd, 'e) some_passive" | SP2 'b | SP3 'c | SP4 'd | SP5 'e
 
-codata lambda =
+codatatype lambda =
   Var string |
   App lambda lambda |
   Abs string lambda |
   Let "(string \<times> lambda) fset" lambda
 
-codata 'a par_lambda =
+codatatype 'a par_lambda =
   PVar 'a |
   PApp "'a par_lambda" "'a par_lambda" |
   PAbs 'a "'a par_lambda" |
@@ -40,75 +40,75 @@
   ('a, 'b1, 'b2) F2 = unit + 'b1 * 'b2
 *)
 
-codata 'a J1 = J11 'a "'a J1" | J12 'a "'a J2"
-   and 'a J2 = J21 | J22 "'a J1" "'a J2"
+codatatype 'a J1 = J11 'a "'a J1" | J12 'a "'a J2"
+and 'a J2 = J21 | J22 "'a J1" "'a J2"
 
-codata 'a tree = TEmpty | TNode 'a "'a forest"
-   and 'a forest = FNil | FCons "'a tree" "'a forest"
+codatatype 'a tree = TEmpty | TNode 'a "'a forest"
+and 'a forest = FNil | FCons "'a tree" "'a forest"
 
-codata 'a tree' = TEmpty' | TNode' "'a branch" "'a branch"
-   and 'a branch = Branch 'a "'a tree'"
+codatatype 'a tree' = TEmpty' | TNode' "'a branch" "'a branch"
+and 'a branch = Branch 'a "'a tree'"
 
-codata ('a, 'b) exp = Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp"
-   and ('a, 'b) trm = Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm"
-   and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp"
+codatatype ('a, 'b) exp = Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp"
+and ('a, 'b) trm = Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm"
+and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp"
 
-codata ('a, 'b, 'c) some_killing =
+codatatype ('a, 'b, 'c) some_killing =
   SK "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) some_killing + ('a, 'b, 'c) in_here"
-   and ('a, 'b, 'c) in_here =
+and ('a, 'b, 'c) in_here =
   IH1 'b 'a | IH2 'c
 
-codata ('a, 'b, 'c) some_killing' =
+codatatype ('a, 'b, 'c) some_killing' =
   SK' "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) some_killing' + ('a, 'b, 'c) in_here'"
-   and ('a, 'b, 'c) in_here' =
+and ('a, 'b, 'c) in_here' =
   IH1' 'b | IH2' 'c
 
-codata ('a, 'b, 'c) some_killing'' =
+codatatype ('a, 'b, 'c) some_killing'' =
   SK'' "'a \<Rightarrow> ('a, 'b, 'c) in_here''"
-   and ('a, 'b, 'c) in_here'' =
+and ('a, 'b, 'c) in_here'' =
   IH1'' 'b 'a | IH2'' 'c
 
-codata ('b, 'c) less_killing = LK "'b \<Rightarrow> 'c"
+codatatype ('b, 'c) less_killing = LK "'b \<Rightarrow> 'c"
 
-codata 'b cps = CPS1 'b | CPS2 "'b \<Rightarrow> 'b cps"
+codatatype 'b cps = CPS1 'b | CPS2 "'b \<Rightarrow> 'b cps"
 
-codata ('b1, 'b2, 'b3, 'b4, 'b5, 'b6, 'b7, 'b8, 'b9) fun_rhs =
+codatatype ('b1, 'b2, 'b3, 'b4, 'b5, 'b6, 'b7, 'b8, 'b9) fun_rhs =
   FR "'b1 \<Rightarrow> 'b2 \<Rightarrow> 'b3 \<Rightarrow> 'b4 \<Rightarrow> 'b5 \<Rightarrow> 'b6 \<Rightarrow> 'b7 \<Rightarrow> 'b8 \<Rightarrow> 'b9 \<Rightarrow>
       ('b1, 'b2, 'b3, 'b4, 'b5, 'b6, 'b7, 'b8, 'b9) fun_rhs"
 
-codata ('b1, 'b2, 'b3, 'b4, 'b5, 'b6, 'b7, 'b8, 'b9, 'b10, 'b11, 'b12, 'b13, 'b14, 'b15, 'b16, 'b17,
+codatatype ('b1, 'b2, 'b3, 'b4, 'b5, 'b6, 'b7, 'b8, 'b9, 'b10, 'b11, 'b12, 'b13, 'b14, 'b15, 'b16, 'b17,
         'b18, 'b19, 'b20) fun_rhs' =
   FR' "'b1 \<Rightarrow> 'b2 \<Rightarrow> 'b3 \<Rightarrow> 'b4 \<Rightarrow> 'b5 \<Rightarrow> 'b6 \<Rightarrow> 'b7 \<Rightarrow> 'b8 \<Rightarrow> 'b9 \<Rightarrow> 'b10 \<Rightarrow> 'b11 \<Rightarrow> 'b12 \<Rightarrow> 'b13 \<Rightarrow> 'b14 \<Rightarrow>
        'b15 \<Rightarrow> 'b16 \<Rightarrow> 'b17 \<Rightarrow> 'b18 \<Rightarrow> 'b19 \<Rightarrow> 'b20 \<Rightarrow>
        ('b1, 'b2, 'b3, 'b4, 'b5, 'b6, 'b7, 'b8, 'b9, 'b10, 'b11, 'b12, 'b13, 'b14, 'b15, 'b16, 'b17,
         'b18, 'b19, 'b20) fun_rhs'"
 
-codata ('a, 'b, 'c) wit3_F1 = W1 'a "('a, 'b, 'c) wit3_F1" "('a, 'b, 'c) wit3_F2"
-   and ('a, 'b, 'c) wit3_F2 = W2 'b "('a, 'b, 'c) wit3_F2"
-   and ('a, 'b, 'c) wit3_F3 = W31 'a 'b "('a, 'b, 'c) wit3_F1" | W32 'c 'a 'b "('a, 'b, 'c) wit3_F1"
+codatatype ('a, 'b, 'c) wit3_F1 = W1 'a "('a, 'b, 'c) wit3_F1" "('a, 'b, 'c) wit3_F2"
+and ('a, 'b, 'c) wit3_F2 = W2 'b "('a, 'b, 'c) wit3_F2"
+and ('a, 'b, 'c) wit3_F3 = W31 'a 'b "('a, 'b, 'c) wit3_F1" | W32 'c 'a 'b "('a, 'b, 'c) wit3_F1"
 
-codata ('c, 'e, 'g) coind_wit1 =
+codatatype ('c, 'e, 'g) coind_wit1 =
        CW1 'c "('c, 'e, 'g) coind_wit1" "('c, 'e, 'g) ind_wit" "('c, 'e, 'g) coind_wit2"
-   and ('c, 'e, 'g) coind_wit2 =
+and ('c, 'e, 'g) coind_wit2 =
        CW21 "('c, 'e, 'g) coind_wit2" 'e | CW22 'c 'g
-   and ('c, 'e, 'g) ind_wit =
+and ('c, 'e, 'g) ind_wit =
        IW1 | IW2 'c
 
-codata ('b, 'a) bar = BAR "'a \<Rightarrow> 'b"
-codata ('a, 'b, 'c, 'd) foo = FOO "'d + 'b \<Rightarrow> 'c + 'a"
+codatatype ('b, 'a) bar = BAR "'a \<Rightarrow> 'b"
+codatatype ('a, 'b, 'c, 'd) foo = FOO "'d + 'b \<Rightarrow> 'c + 'a"
 
-codata 'a dead_foo = A
-codata ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo"
+codatatype 'a dead_foo = A
+codatatype ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo"
 
 (* SLOW, MEMORY-HUNGRY
-codata ('a, 'c) D1 = A1 "('a, 'c) D2" | B1 "'a list"
-   and ('a, 'c) D2 = A2 "('a, 'c) D3" | B2 "'c list"
-   and ('a, 'c) D3 = A3 "('a, 'c) D3" | B3 "('a, 'c) D4" | C3 "('a, 'c) D4" "('a, 'c) D5"
-   and ('a, 'c) D4 = A4 "('a, 'c) D5" | B4 "'a list list list"
-   and ('a, 'c) D5 = A5 "('a, 'c) D6"
-   and ('a, 'c) D6 = A6 "('a, 'c) D7"
-   and ('a, 'c) D7 = A7 "('a, 'c) D8"
-   and ('a, 'c) D8 = A8 "('a, 'c) D1 list"
+codatatype ('a, 'c) D1 = A1 "('a, 'c) D2" | B1 "'a list"
+and ('a, 'c) D2 = A2 "('a, 'c) D3" | B2 "'c list"
+and ('a, 'c) D3 = A3 "('a, 'c) D3" | B3 "('a, 'c) D4" | C3 "('a, 'c) D4" "('a, 'c) D5"
+and ('a, 'c) D4 = A4 "('a, 'c) D5" | B4 "'a list list list"
+and ('a, 'c) D5 = A5 "('a, 'c) D6"
+and ('a, 'c) D6 = A6 "('a, 'c) D7"
+and ('a, 'c) D7 = A7 "('a, 'c) D8"
+and ('a, 'c) D8 = A8 "('a, 'c) D1 list"
 *)
 
 end

--- a/src/HOL/BNF/Examples/Misc_Data.thy	Mon Apr 29 06:13:36 2013 +0200
+++ b/src/HOL/BNF/Examples/Misc_Data.thy	Mon Apr 29 09:10:49 2013 +0200
@@ -13,24 +13,24 @@
 imports "../BNF"
 begin
 
-data simple = X1 | X2 | X3 | X4
+datatype_new simple = X1 | X2 | X3 | X4
 
-data simple' = X1' unit | X2' unit | X3' unit | X4' unit
+datatype_new simple' = X1' unit | X2' unit | X3' unit | X4' unit
 
-data 'a mylist = MyNil | MyCons 'a "'a mylist"
+datatype_new 'a mylist = MyNil | MyCons 'a "'a mylist"
 
-data ('b, 'c, 'd, 'e) some_passive =
+datatype_new ('b, 'c, 'd, 'e) some_passive =
   SP1 "('b, 'c, 'd, 'e) some_passive" | SP2 'b | SP3 'c | SP4 'd | SP5 'e
 
-data hfset = HFset "hfset fset"
+datatype_new hfset = HFset "hfset fset"
 
-data lambda =
+datatype_new lambda =
   Var string |
   App lambda lambda |
   Abs string lambda |
   Let "(string \<times> lambda) fset" lambda
 
-data 'a par_lambda =
+datatype_new 'a par_lambda =
   PVar 'a |
   PApp "'a par_lambda" "'a par_lambda" |
   PAbs 'a "'a par_lambda" |
@@ -41,73 +41,73 @@
   ('a, 'b1, 'b2) F2 = unit + 'b1 * 'b2
 *)
 
-data 'a I1 = I11 'a "'a I1" | I12 'a "'a I2"
- and 'a I2 = I21 | I22 "'a I1" "'a I2"
+datatype_new 'a I1 = I11 'a "'a I1" | I12 'a "'a I2"
+and 'a I2 = I21 | I22 "'a I1" "'a I2"
 
-data 'a tree = TEmpty | TNode 'a "'a forest"
- and 'a forest = FNil | FCons "'a tree" "'a forest"
+datatype_new 'a tree = TEmpty | TNode 'a "'a forest"
+and 'a forest = FNil | FCons "'a tree" "'a forest"
 
-data 'a tree' = TEmpty' | TNode' "'a branch" "'a branch"
- and 'a branch = Branch 'a "'a tree'"
+datatype_new 'a tree' = TEmpty' | TNode' "'a branch" "'a branch"
+and 'a branch = Branch 'a "'a tree'"
 
-data ('a, 'b) exp = Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp"
- and ('a, 'b) trm = Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm"
- and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp"
+datatype_new ('a, 'b) exp = Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp"
+and ('a, 'b) trm = Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm"
+and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp"
 
-data ('a, 'b, 'c) some_killing =
+datatype_new ('a, 'b, 'c) some_killing =
   SK "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) some_killing + ('a, 'b, 'c) in_here"
- and ('a, 'b, 'c) in_here =
+and ('a, 'b, 'c) in_here =
   IH1 'b 'a | IH2 'c
 
-data 'b nofail1 = NF11 "'b nofail1" 'b | NF12 'b
-data 'b nofail2 = NF2 "('b nofail2 \<times> 'b \<times> 'b nofail2 \<times> 'b) list"
-data 'b nofail3 = NF3 'b "('b nofail3 \<times> 'b \<times> 'b nofail3 \<times> 'b) fset"
-data 'b nofail4 = NF4 "('b nofail4 \<times> ('b nofail4 \<times> 'b \<times> 'b nofail4 \<times> 'b) fset) list"
+datatype_new 'b nofail1 = NF11 "'b nofail1" 'b | NF12 'b
+datatype_new 'b nofail2 = NF2 "('b nofail2 \<times> 'b \<times> 'b nofail2 \<times> 'b) list"
+datatype_new 'b nofail3 = NF3 'b "('b nofail3 \<times> 'b \<times> 'b nofail3 \<times> 'b) fset"
+datatype_new 'b nofail4 = NF4 "('b nofail4 \<times> ('b nofail4 \<times> 'b \<times> 'b nofail4 \<times> 'b) fset) list"
 
 (*
-data 'b fail = F "'b fail" 'b "'b fail" "'b list"
-data 'b fail = F "'b fail" 'b "'b fail" 'b
-data 'b fail = F1 "'b fail" 'b | F2 "'b fail"
-data 'b fail = F "'b fail" 'b
+datatype_new 'b fail = F "'b fail" 'b "'b fail" "'b list"
+datatype_new 'b fail = F "'b fail" 'b "'b fail" 'b
+datatype_new 'b fail = F1 "'b fail" 'b | F2 "'b fail"
+datatype_new 'b fail = F "'b fail" 'b
 *)
 
-data l1 = L1 "l2 list"
- and l2 = L21 "l1 fset" | L22 l2
+datatype_new l1 = L1 "l2 list"
+and l2 = L21 "l1 fset" | L22 l2
 
-data kk1 = KK1 kk2
- and kk2 = KK2 kk3
- and kk3 = KK3 "kk1 list"
+datatype_new kk1 = KK1 kk2
+and kk2 = KK2 kk3
+and kk3 = KK3 "kk1 list"
 
-data t1 = T11 t3 | T12 t2
- and t2 = T2 t1
- and t3 = T3
+datatype_new t1 = T11 t3 | T12 t2
+and t2 = T2 t1
+and t3 = T3
 
-data t1' = T11' t2' | T12' t3'
- and t2' = T2' t1'
- and t3' = T3'
+datatype_new t1' = T11' t2' | T12' t3'
+and t2' = T2' t1'
+and t3' = T3'
 
 (*
-data fail1 = F1 fail2
- and fail2 = F2 fail3
- and fail3 = F3 fail1
+datatype_new fail1 = F1 fail2
+and fail2 = F2 fail3
+and fail3 = F3 fail1
 
-data fail1 = F1 "fail2 list" fail2
- and fail2 = F2 "fail2 fset" fail3
- and fail3 = F3 fail1
+datatype_new fail1 = F1 "fail2 list" fail2
+and fail2 = F2 "fail2 fset" fail3
+and fail3 = F3 fail1
 
-data fail1 = F1 "fail2 list" fail2
- and fail2 = F2 "fail1 fset" fail1
+datatype_new fail1 = F1 "fail2 list" fail2
+and fail2 = F2 "fail1 fset" fail1
 *)
 
 (* SLOW
-data ('a, 'c) D1 = A1 "('a, 'c) D2" | B1 "'a list"
- and ('a, 'c) D2 = A2 "('a, 'c) D3" | B2 "'c list"
- and ('a, 'c) D3 = A3 "('a, 'c) D3" | B3 "('a, 'c) D4" | C3 "('a, 'c) D4" "('a, 'c) D5"
- and ('a, 'c) D4 = A4 "('a, 'c) D5" | B4 "'a list list list"
- and ('a, 'c) D5 = A5 "('a, 'c) D6"
- and ('a, 'c) D6 = A6 "('a, 'c) D7"
- and ('a, 'c) D7 = A7 "('a, 'c) D8"
- and ('a, 'c) D8 = A8 "('a, 'c) D1 list"
+datatype_new ('a, 'c) D1 = A1 "('a, 'c) D2" | B1 "'a list"
+and ('a, 'c) D2 = A2 "('a, 'c) D3" | B2 "'c list"
+and ('a, 'c) D3 = A3 "('a, 'c) D3" | B3 "('a, 'c) D4" | C3 "('a, 'c) D4" "('a, 'c) D5"
+and ('a, 'c) D4 = A4 "('a, 'c) D5" | B4 "'a list list list"
+and ('a, 'c) D5 = A5 "('a, 'c) D6"
+and ('a, 'c) D6 = A6 "('a, 'c) D7"
+and ('a, 'c) D7 = A7 "('a, 'c) D8"
+and ('a, 'c) D8 = A8 "('a, 'c) D1 list"
 
 (*time comparison*)
 datatype ('a, 'c) D1' = A1' "('a, 'c) D2'" | B1' "'a list"
@@ -121,58 +121,58 @@
 *)
 
 (* fail:
-data tt1 = TT11 tt2 tt3 | TT12 tt2 tt4
- and tt2 = TT2
- and tt3 = TT3 tt4
- and tt4 = TT4 tt1
+datatype_new tt1 = TT11 tt2 tt3 | TT12 tt2 tt4
+and tt2 = TT2
+and tt3 = TT3 tt4
+and tt4 = TT4 tt1
 *)
 
-data k1 = K11 k2 k3 | K12 k2 k4
- and k2 = K2
- and k3 = K3 k4
- and k4 = K4
+datatype_new k1 = K11 k2 k3 | K12 k2 k4
+and k2 = K2
+and k3 = K3 k4
+and k4 = K4
 
-data tt1 = TT11 tt3 tt2 | TT12 tt2 tt4
- and tt2 = TT2
- and tt3 = TT3 tt1
- and tt4 = TT4
+datatype_new tt1 = TT11 tt3 tt2 | TT12 tt2 tt4
+and tt2 = TT2
+and tt3 = TT3 tt1
+and tt4 = TT4
 
 (* SLOW
-data s1 = S11 s2 s3 s4 | S12 s3 | S13 s2 s6 | S14 s4 s2 | S15 s2 s2
- and s2 = S21 s7 s5 | S22 s5 s4 s6
- and s3 = S31 s1 s7 s2 | S32 s3 s3 | S33 s4 s5
- and s4 = S4 s5
- and s5 = S5
- and s6 = S61 s6 | S62 s1 s2 | S63 s6
- and s7 = S71 s8 | S72 s5
- and s8 = S8 nat
+datatype_new s1 = S11 s2 s3 s4 | S12 s3 | S13 s2 s6 | S14 s4 s2 | S15 s2 s2
+and s2 = S21 s7 s5 | S22 s5 s4 s6
+and s3 = S31 s1 s7 s2 | S32 s3 s3 | S33 s4 s5
+and s4 = S4 s5
+and s5 = S5
+and s6 = S61 s6 | S62 s1 s2 | S63 s6
+and s7 = S71 s8 | S72 s5
+and s8 = S8 nat
 *)
 
-data ('a, 'b) bar = Bar "'b \<Rightarrow> 'a"
-data ('a, 'b, 'c, 'd) foo = Foo "'d + 'b \<Rightarrow> 'c + 'a"
+datatype_new ('a, 'b) bar = Bar "'b \<Rightarrow> 'a"
+datatype_new ('a, 'b, 'c, 'd) foo = Foo "'d + 'b \<Rightarrow> 'c + 'a"
 
-data 'a dead_foo = A
-data ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo"
+datatype_new 'a dead_foo = A
+datatype_new ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo"
 
-data d1 = D
-data d1' = is_D: D
+datatype_new d1 = D
+datatype_new d1' = is_D: D
 
-data d2 = D nat
-data d2' = is_D: D nat
+datatype_new d2 = D nat
+datatype_new d2' = is_D: D nat
 
-data d3 = D | E
-data d3' = D | is_E: E
-data d3'' = is_D: D | E
-data d3''' = is_D: D | is_E: E
+datatype_new d3 = D | E
+datatype_new d3' = D | is_E: E
+datatype_new d3'' = is_D: D | E
+datatype_new d3''' = is_D: D | is_E: E
 
-data d4 = D nat | E
-data d4' = D nat | is_E: E
-data d4'' = is_D: D nat | E
-data d4''' = is_D: D nat | is_E: E
+datatype_new d4 = D nat | E
+datatype_new d4' = D nat | is_E: E
+datatype_new d4'' = is_D: D nat | E
+datatype_new d4''' = is_D: D nat | is_E: E
 
-data d5 = D nat | E int
-data d5' = D nat | is_E: E int
-data d5'' = is_D: D nat | E int
-data d5''' = is_D: D nat | is_E: E int
+datatype_new d5 = D nat | E int
+datatype_new d5' = D nat | is_E: E int
+datatype_new d5'' = is_D: D nat | E int
+datatype_new d5''' = is_D: D nat | is_E: E int
 
 end

--- a/src/HOL/BNF/Examples/Process.thy	Mon Apr 29 06:13:36 2013 +0200
+++ b/src/HOL/BNF/Examples/Process.thy	Mon Apr 29 09:10:49 2013 +0200
@@ -13,7 +13,7 @@
 
 hide_fact (open) Quotient_Product.prod_rel_def
 
-codata 'a process =
+codatatype 'a process =
   isAction: Action (prefOf: 'a) (contOf: "'a process") |
   isChoice: Choice (ch1Of: "'a process") (ch2Of: "'a process")
 

--- a/src/HOL/BNF/Examples/Stream.thy	Mon Apr 29 06:13:36 2013 +0200
+++ b/src/HOL/BNF/Examples/Stream.thy	Mon Apr 29 09:10:49 2013 +0200
@@ -12,8 +12,8 @@
 imports "../BNF"
 begin
 
-codata (sset: 'a) stream (map: smap rel: stream_all2) =
-   Stream (shd: 'a) (stl: "'a stream") (infixr "##" 65)
+codatatype (sset: 'a) stream (map: smap rel: stream_all2) =
+  Stream (shd: 'a) (stl: "'a stream") (infixr "##" 65)
 
 declaration {*
   Nitpick_HOL.register_codatatype

--- a/src/HOL/BNF/Examples/TreeFI.thy	Mon Apr 29 06:13:36 2013 +0200
+++ b/src/HOL/BNF/Examples/TreeFI.thy	Mon Apr 29 09:10:49 2013 +0200
@@ -12,7 +12,7 @@
 imports ListF
 begin
 
-codata 'a treeFI = Tree (lab: 'a) (sub: "'a treeFI listF")
+codatatype 'a treeFI = Tree (lab: 'a) (sub: "'a treeFI listF")
 
 lemma pre_treeFI_listF_set[simp]: "pre_treeFI_set2 (i, xs) = listF_set xs"
 unfolding pre_treeFI_set2_def collect_def[abs_def] prod_set_defs

--- a/src/HOL/BNF/Examples/TreeFsetI.thy	Mon Apr 29 06:13:36 2013 +0200
+++ b/src/HOL/BNF/Examples/TreeFsetI.thy	Mon Apr 29 09:10:49 2013 +0200
@@ -14,7 +14,7 @@
 
 hide_fact (open) Quotient_Product.prod_rel_def
 
-codata 'a treeFsetI = Tree (lab: 'a) (sub: "'a treeFsetI fset")
+codatatype 'a treeFsetI = Tree (lab: 'a) (sub: "'a treeFsetI fset")
 
 definition pair_fun (infixr "\<odot>" 50) where
   "f \<odot> g \<equiv> \<lambda>x. (f x, g x)"

--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Apr 29 06:13:36 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Apr 29 09:10:49 2013 +0200
@@ -159,7 +159,6 @@
     (wrap_opts as (no_dests, rep_compat), specs) no_defs_lthy0 =
   let
     (* TODO: sanity checks on arguments *)
-    (* TODO: integration with function package ("size") *)
 
     val _ = if not lfp andalso no_dests then error "Cannot define destructor-less codatatypes"
       else ();

--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Mon Apr 29 06:13:36 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Mon Apr 29 09:10:49 2013 +0200
@@ -3036,7 +3036,7 @@
   end;
 
 val _ =
-  Outer_Syntax.local_theory @{command_spec "codata"} "define BNF-based coinductive datatypes"
+  Outer_Syntax.local_theory @{command_spec "codatatype"} "define BNF-based coinductive datatypes"
     (parse_datatype_cmd false construct_gfp);
 
 end;

--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Mon Apr 29 06:13:36 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Mon Apr 29 09:10:49 2013 +0200
@@ -1860,7 +1860,7 @@
   end;
 
 val _ =
-  Outer_Syntax.local_theory @{command_spec "data"} "define BNF-based inductive datatypes"
+  Outer_Syntax.local_theory @{command_spec "datatype_new"} "define BNF-based inductive datatypes"
     (parse_datatype_cmd true construct_lfp);
 
 end;