# HG changeset patch
# User traytel
# Date 1409658003 -7200
# Node ID e4c69c0985f5d837ff5d2e8014a058c0e0b6b28d
# Parent  3bfd12e456f42decd7ce12703c6e74e3339f9295
test discriminators/selectors in BNF regression suite

diff -r 3bfd12e456f4 -r e4c69c0985f5 src/HOL/BNF_Examples/IsaFoR_Datatypes.thy
--- a/src/HOL/BNF_Examples/IsaFoR_Datatypes.thy	Tue Sep 02 12:13:32 2014 +0200
+++ b/src/HOL/BNF_Examples/IsaFoR_Datatypes.thy	Tue Sep 02 13:40:03 2014 +0200
@@ -11,16 +11,16 @@
 imports Real
 begin
 
-datatype_new ('f, 'l) lab =
+datatype_new (discs_sels) ('f, 'l) lab =
     Lab "('f, 'l) lab" 'l
   | FunLab "('f, 'l) lab" "('f, 'l) lab list"
   | UnLab 'f
   | Sharp "('f, 'l) lab"
 
-datatype_new 'f projL = Projection "(('f \<times> nat) \<times> nat) list"
+datatype_new (discs_sels) 'f projL = Projection "(('f \<times> nat) \<times> nat) list"
 
-datatype_new ('f, 'v) "term" = Var 'v | Fun 'f "('f, 'v) term list"
-datatype_new ('f, 'v) ctxt =
+datatype_new (discs_sels) ('f, 'v) "term" = Var 'v | Fun 'f "('f, 'v) term list"
+datatype_new (discs_sels) ('f, 'v) ctxt =
     Hole ("\<box>")
   | More 'f "('f, 'v) term list" "('f, 'v) ctxt" "('f, 'v) term list"
 
@@ -32,7 +32,7 @@
 type_synonym ('f, 'l, 'v) trsLL   = "(('f, 'l) lab, 'v) rules"
 type_synonym ('f, 'l, 'v) termsLL = "(('f, 'l) lab, 'v) term list"
 
-datatype_new pos = Empty ("\<epsilon>") | PCons "nat" "pos" (infixr "<#" 70)
+datatype_new (discs_sels) pos = Empty ("\<epsilon>") | PCons "nat" "pos" (infixr "<#" 70)
 
 type_synonym  ('f, 'v) prseq = "(pos \<times> ('f, 'v) rule \<times> bool \<times> ('f, 'v) term) list"
 type_synonym  ('f, 'v) rseq = "(pos \<times> ('f, 'v) rule \<times> ('f, 'v) term) list"
@@ -49,7 +49,7 @@
 type_synonym ('f, 'l, 'v) qtrsLL =
   "bool \<times> ('f, 'l, 'v) termsLL \<times> ('f, 'l, 'v) trsLL"
 
-datatype_new location = H | A | B | R
+datatype_new (discs_sels) location = H | A | B | R
 
 type_synonym ('f, 'v) forb_pattern = "('f, 'v) ctxt \<times> ('f, 'v) term \<times> location"
 type_synonym ('f, 'v) forb_patterns = "('f, 'v) forb_pattern set"
@@ -68,20 +68,20 @@
 type_synonym 'a vec = "'a list"
 type_synonym 'a mat = "'a vec list"
 
-datatype_new arctic = MinInfty | Num_arc int
-datatype_new 'a arctic_delta = MinInfty_delta | Num_arc_delta 'a
-datatype_new order_tag = Lex | Mul
+datatype_new (discs_sels) arctic = MinInfty | Num_arc int
+datatype_new (discs_sels) 'a arctic_delta = MinInfty_delta | Num_arc_delta 'a
+datatype_new (discs_sels) order_tag = Lex | Mul
 
 type_synonym 'f status_prec_repr = "(('f \<times> nat) \<times> (nat \<times> order_tag)) list"
 
-datatype_new af_entry =
+datatype_new (discs_sels) af_entry =
     Collapse nat
   | AFList "nat list"
 
 type_synonym 'f afs_list = "(('f \<times> nat) \<times> af_entry) list"
 type_synonym 'f prec_weight_repr = "(('f \<times> nat) \<times> (nat \<times> nat \<times> (nat list option))) list \<times> nat"
 
-datatype_new 'f redtriple_impl =
+datatype_new (discs_sels) 'f redtriple_impl =
     Int_carrier "('f, int) lpoly_interL"
   | Int_nl_carrier "('f, int) poly_inter_list"
   | Rat_carrier "('f, rat) lpoly_interL"
@@ -98,15 +98,15 @@
   | RPO "'f status_prec_repr" "'f afs_list"
   | KBO "'f prec_weight_repr" "'f afs_list"
 
-datatype_new list_order_type = MS_Ext | Max_Ext | Min_Ext  | Dms_Ext
+datatype_new (discs_sels) list_order_type = MS_Ext | Max_Ext | Min_Ext  | Dms_Ext
 type_synonym 'f scnp_af = "(('f \<times> nat) \<times> (nat \<times> nat) list) list"
 
-datatype_new 'f root_redtriple_impl = SCNP list_order_type "'f scnp_af" "'f redtriple_impl"
+datatype_new (discs_sels) 'f root_redtriple_impl = SCNP list_order_type "'f scnp_af" "'f redtriple_impl"
 
 type_synonym 'f sig_map_list = "(('f \<times> nat) \<times> 'f list) list"
 type_synonym ('f, 'v) uncurry_info = "'f \<times> 'f sig_map_list \<times> ('f, 'v) rules \<times> ('f, 'v) rules"
 
-datatype_new arithFun =
+datatype_new (discs_sels) arithFun =
     Arg nat
   | Const nat
   | Sum "arithFun list"
@@ -115,25 +115,25 @@
   | Prod "arithFun list"
   | IfEqual arithFun arithFun arithFun arithFun
 
-datatype_new 'f sl_inter = SL_Inter nat "(('f \<times> nat) \<times> arithFun) list"
-datatype_new ('f, 'v) sl_variant =
+datatype_new (discs_sels) 'f sl_inter = SL_Inter nat "(('f \<times> nat) \<times> arithFun) list"
+datatype_new (discs_sels) ('f, 'v) sl_variant =
     Rootlab "('f \<times> nat) option"
   | Finitelab "'f sl_inter"
   | QuasiFinitelab "'f sl_inter" 'v
 
 type_synonym ('f, 'v) crit_pair_joins = "(('f, 'v) term \<times> ('f, 'v) rseq \<times> ('f, 'v) term \<times> ('f, 'v) rseq) list"
 
-datatype_new 'f join_info = Guided "('f, string) crit_pair_joins" | Join_NF | Join_BFS nat
+datatype_new (discs_sels) 'f join_info = Guided "('f, string) crit_pair_joins" | Join_NF | Join_BFS nat
 
 type_synonym unknown_info = string
 
 type_synonym dummy_prf = unit
 
-datatype_new ('f, 'v) complex_constant_removal_prf = Complex_Constant_Removal_Proof
+datatype_new (discs_sels) ('f, 'v) complex_constant_removal_prf = Complex_Constant_Removal_Proof
   "('f, 'v) term"
   "(('f, 'v) rule \<times> ('f, 'v) rule) list"
 
-datatype_new ('f, 'v) cond_constraint =
+datatype_new (discs_sels) ('f, 'v) cond_constraint =
     CC_cond bool "('f, 'v) rule"
   | CC_rewr "('f, 'v) term" "('f, 'v) term"
   | CC_impl "('f, 'v) cond_constraint list" "('f, 'v) cond_constraint"
@@ -142,7 +142,7 @@
 type_synonym ('f, 'v, 'w) gsubstL = "('v \<times> ('f, 'w) term) list"
 type_synonym ('f, 'v) substL = "('f, 'v, 'v) gsubstL"
 
-datatype_new ('f, 'v) cond_constraint_prf =
+datatype_new (discs_sels) ('f, 'v) cond_constraint_prf =
     Final
   | Delete_Condition "('f, 'v) cond_constraint" "('f, 'v) cond_constraint_prf"
   | Different_Constructor "('f, 'v) cond_constraint"
@@ -152,28 +152,28 @@
   | Simplify_Condition "('f, 'v) cond_constraint" "('f, 'v) substL" "('f, 'v) cond_constraint" "('f, 'v) cond_constraint_prf"
   | Induction "('f, 'v) cond_constraint" "('f, 'v) cond_constraint list" "(('f, 'v) rule \<times> (('f, 'v) term \<times> 'v list) list \<times> ('f, 'v) cond_constraint \<times> ('f, 'v) cond_constraint_prf) list"
 
-datatype_new ('f, 'v) cond_red_pair_prf =
+datatype_new (discs_sels) ('f, 'v) cond_red_pair_prf =
   Cond_Red_Pair_Prf
     'f "(('f, 'v) cond_constraint \<times> ('f, 'v) rules \<times> ('f, 'v) cond_constraint_prf) list" nat nat
 
-datatype_new ('q, 'f) ta_rule = TA_rule 'f "'q list" 'q ("_ _ \<rightarrow> _")
-datatype_new ('q, 'f) tree_automaton = Tree_Automaton "'q list" "('q, 'f) ta_rule list" "('q \<times> 'q) list"
-datatype_new 'q ta_relation =
+datatype_new (discs_sels) ('q, 'f) ta_rule = TA_rule 'f "'q list" 'q ("_ _ \<rightarrow> _")
+datatype_new (discs_sels) ('q, 'f) tree_automaton = Tree_Automaton "'q list" "('q, 'f) ta_rule list" "('q \<times> 'q) list"
+datatype_new (discs_sels) 'q ta_relation =
     Decision_Proc
   | Id_Relation
   | Some_Relation "('q \<times> 'q) list"
 
-datatype_new boundstype = Roof | Match
-datatype_new ('f, 'q) bounds_info = Bounds_Info boundstype nat "'q list" "('q, 'f \<times> nat) tree_automaton" "'q ta_relation"
+datatype_new (discs_sels) boundstype = Roof | Match
+datatype_new (discs_sels) ('f, 'q) bounds_info = Bounds_Info boundstype nat "'q list" "('q, 'f \<times> nat) tree_automaton" "'q ta_relation"
 
-datatype_new ('f, 'v) pat_eqv_prf =
+datatype_new (discs_sels) ('f, 'v) pat_eqv_prf =
     Pat_Dom_Renaming "('f, 'v) substL"
   | Pat_Irrelevant "('f, 'v) substL" "('f, 'v) substL"
   | Pat_Simplify "('f, 'v) substL" "('f, 'v) substL"
 
-datatype_new pat_rule_pos = Pat_Base | Pat_Pump | Pat_Close
+datatype_new (discs_sels) pat_rule_pos = Pat_Base | Pat_Pump | Pat_Close
 
-datatype_new ('f, 'v) pat_rule_prf =
+datatype_new (discs_sels) ('f, 'v) pat_rule_prf =
     Pat_OrigRule "('f, 'v) rule" bool
   | Pat_InitPump "('f, 'v) pat_rule_prf" "('f, 'v) substL" "('f, 'v) substL"
   | Pat_InitPumpCtxt "('f, 'v) pat_rule_prf" "('f, 'v) substL" pos 'v
@@ -183,10 +183,10 @@
   | Pat_Rewr "('f, 'v) pat_rule_prf" "('f, 'v) term \<times> ('f, 'v) rseq" pat_rule_pos 'v
   | Pat_Exp_Sigma "('f, 'v) pat_rule_prf" nat
 
-datatype_new ('f, 'v) non_loop_prf =
+datatype_new (discs_sels) ('f, 'v) non_loop_prf =
     Non_Loop_Prf "('f, 'v) pat_rule_prf" "('f, 'v) substL" "('f, 'v) substL" nat nat pos
 
-datatype_new ('f, 'l, 'v) problem =
+datatype_new (discs_sels) ('f, 'l, 'v) problem =
     SN_TRS "('f, 'l, 'v) qreltrsLL"
   | SN_FP_TRS "('f, 'l, 'v) fptrsLL"
   | Finite_DPP "('f, 'l, 'v) dppLL"
@@ -198,7 +198,7 @@
 
 declare [[bnf_timing]]
 
-datatype_new ('f, 'l, 'v, 'a, 'b, 'c, 'd, 'e) generic_assm_proof =
+datatype_new (discs_sels) ('f, 'l, 'v, 'a, 'b, 'c, 'd, 'e) generic_assm_proof =
     SN_assm_proof "('f, 'l, 'v) qreltrsLL" 'a
   | Finite_assm_proof "('f, 'l, 'v) dppLL" 'b
   | SN_FP_assm_proof "('f, 'l, 'v) fptrsLL" 'c
@@ -210,7 +210,7 @@
 
 type_synonym ('f, 'l, 'v, 'a, 'b, 'c, 'd) assm_proof = "('f, 'l, 'v, 'a, 'b, 'c, dummy_prf, 'd) generic_assm_proof"
 
-datatype_new ('f, 'l, 'v) assm =
+datatype_new (discs_sels) ('f, 'l, 'v) assm =
     SN_assm "('f, 'l, 'v) problem list" "('f, 'l, 'v) qreltrsLL"
   | SN_FP_assm "('f, 'l, 'v) problem list" "('f, 'l, 'v) fptrsLL"
   | Finite_assm "('f, 'l, 'v) problem list" "('f, 'l, 'v) dppLL"
@@ -254,7 +254,7 @@
 | "collect_neg_assms tp dpp rtp fptp unk (Unknown_assm_proof p prf) = unk prf"
 | "collect_neg_assms tp dpp rtp fptp unk _ = []"
 
-datatype_new ('f, 'l, 'v) dp_nontermination_proof =
+datatype_new (discs_sels) ('f, 'l, 'v) dp_nontermination_proof =
     DP_Loop "(('f, 'l) lab, 'v) term" "(('f, 'l) lab, 'v) prseq" "(('f, 'l) lab, 'v) substL" "(('f, 'l) lab, 'v) ctxt"
   | DP_Nonloop "(('f, 'l) lab, 'v) non_loop_prf"
   | DP_Rule_Removal "('f, 'l, 'v) trsLL option" "('f, 'l, 'v) trsLL option" "('f, 'l, 'v) dp_nontermination_proof"
@@ -312,7 +312,7 @@
        ('f, 'l, 'v) fp_nontermination_proof,
        ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list"
 
-datatype_new ('f, 'l, 'v) dp_termination_proof =
+datatype_new (discs_sels) ('f, 'l, 'v) dp_termination_proof =
     P_is_Empty
   | Subterm_Criterion_Proc "('f, 'l) lab projL" "('f, 'l, 'v) rseqL"
       "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
diff -r 3bfd12e456f4 -r e4c69c0985f5 src/HOL/BNF_Examples/Misc_Datatype.thy
--- a/src/HOL/BNF_Examples/Misc_Datatype.thy	Tue Sep 02 12:13:32 2014 +0200
+++ b/src/HOL/BNF_Examples/Misc_Datatype.thy	Tue Sep 02 13:40:03 2014 +0200
@@ -13,26 +13,26 @@
 imports "~~/src/HOL/Library/FSet"
 begin
 
-datatype_new simple = X1 | X2 | X3 | X4
+datatype_new (discs_sels) simple = X1 | X2 | X3 | X4
 
-datatype_new simple' = X1' unit | X2' unit | X3' unit | X4' unit
+datatype_new (discs_sels) simple' = X1' unit | X2' unit | X3' unit | X4' unit
 
-datatype_new simple'' = X1'' nat int | X2''
+datatype_new (discs_sels) simple'' = X1'' nat int | X2''
 
-datatype_new 'a mylist = MyNil | MyCons (myhd: 'a) (mytl: "'a mylist")
+datatype_new (discs_sels) 'a mylist = MyNil | MyCons (myhd: 'a) (mytl: "'a mylist")
 
-datatype_new ('b, 'c, 'd, 'e) some_passive =
+datatype_new (discs_sels) ('b, 'c, 'd, 'e) some_passive =
   SP1 "('b, 'c, 'd, 'e) some_passive" | SP2 'b | SP3 'c | SP4 'd | SP5 'e
 
-datatype_new hfset = HFset "hfset fset"
+datatype_new (discs_sels) hfset = HFset "hfset fset"
 
-datatype_new lambda =
+datatype_new (discs_sels) lambda =
   Var string |
   App lambda lambda |
   Abs string lambda |
   Let "(string \<times> lambda) fset" lambda
 
-datatype_new 'a par_lambda =
+datatype_new (discs_sels) 'a par_lambda =
   PVar 'a |
   PApp "'a par_lambda" "'a par_lambda" |
   PAbs 'a "'a par_lambda" |
@@ -43,70 +43,70 @@
   ('a, 'b1, 'b2) F2 = unit + 'b1 * 'b2
 *)
 
-datatype_new 'a I1 = I11 'a "'a I1" | I12 'a "'a I2"
+datatype_new (discs_sels) 'a I1 = I11 'a "'a I1" | I12 'a "'a I2"
 and 'a I2 = I21 | I22 "'a I1" "'a I2"
 
-datatype_new 'a tree = TEmpty | TNode 'a "'a forest"
+datatype_new (discs_sels) 'a tree = TEmpty | TNode 'a "'a forest"
 and 'a forest = FNil | FCons "'a tree" "'a forest"
 
-datatype_new 'a tree' = TEmpty' | TNode' "'a branch" "'a branch"
+datatype_new (discs_sels) 'a tree' = TEmpty' | TNode' "'a branch" "'a branch"
 and 'a branch = Branch 'a "'a tree'"
 
-datatype_new 'a bin_rose_tree = BRTree 'a "'a bin_rose_tree mylist" "'a bin_rose_tree mylist"
+datatype_new (discs_sels) 'a bin_rose_tree = BRTree 'a "'a bin_rose_tree mylist" "'a bin_rose_tree mylist"
 
-datatype_new ('a, 'b) exp = Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp"
+datatype_new (discs_sels) ('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 ftree = FTLeaf 'a | FTNode "'a \<Rightarrow> 'a ftree"
+datatype_new (discs_sels) 'a ftree = FTLeaf 'a | FTNode "'a \<Rightarrow> 'a ftree"
 
-datatype_new ('a, 'b, 'c) some_killing =
+datatype_new (discs_sels) ('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 =
   IH1 'b 'a | IH2 'c
 
-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"
+datatype_new (discs_sels) 'b nofail1 = NF11 "'b nofail1" 'b | NF12 'b
+datatype_new (discs_sels) 'b nofail2 = NF2 "('b nofail2 \<times> 'b \<times> 'b nofail2 \<times> 'b) list"
+datatype_new (discs_sels) 'b nofail3 = NF3 'b "('b nofail3 \<times> 'b \<times> 'b nofail3 \<times> 'b) fset"
+datatype_new (discs_sels) 'b nofail4 = NF4 "('b nofail4 \<times> ('b nofail4 \<times> 'b \<times> 'b nofail4 \<times> 'b) fset) list"
 
 (*
-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
+datatype_new (discs_sels) 'b fail = F "'b fail" 'b "'b fail" "'b list"
+datatype_new (discs_sels) 'b fail = F "'b fail" 'b "'b fail" 'b
+datatype_new (discs_sels) 'b fail = F1 "'b fail" 'b | F2 "'b fail"
+datatype_new (discs_sels) 'b fail = F "'b fail" 'b
 *)
 
-datatype_new l1 = L1 "l2 list"
+datatype_new (discs_sels) l1 = L1 "l2 list"
 and l2 = L21 "l1 fset" | L22 l2
 
-datatype_new kk1 = KK1 kk2
+datatype_new (discs_sels) kk1 = KK1 kk2
 and kk2 = KK2 kk3
 and kk3 = KK3 "kk1 list"
 
-datatype_new t1 = T11 t3 | T12 t2
+datatype_new (discs_sels) t1 = T11 t3 | T12 t2
 and t2 = T2 t1
 and t3 = T3
 
-datatype_new t1' = T11' t2' | T12' t3'
+datatype_new (discs_sels) t1' = T11' t2' | T12' t3'
 and t2' = T2' t1'
 and t3' = T3'
 
 (*
-datatype_new fail1 = F1 fail2
+datatype_new (discs_sels) fail1 = F1 fail2
 and fail2 = F2 fail3
 and fail3 = F3 fail1
 
-datatype_new fail1 = F1 "fail2 list" fail2
+datatype_new (discs_sels) fail1 = F1 "fail2 list" fail2
 and fail2 = F2 "fail2 fset" fail3
 and fail3 = F3 fail1
 
-datatype_new fail1 = F1 "fail2 list" fail2
+datatype_new (discs_sels) fail1 = F1 "fail2 list" fail2
 and fail2 = F2 "fail1 fset" fail1
 *)
 
 (* SLOW
-datatype_new ('a, 'c) D1 = A1 "('a, 'c) D2" | B1 "'a list"
+datatype_new (discs_sels) ('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"
@@ -127,24 +127,24 @@
 *)
 
 (* fail:
-datatype_new tt1 = TT11 tt2 tt3 | TT12 tt2 tt4
+datatype_new (discs_sels) tt1 = TT11 tt2 tt3 | TT12 tt2 tt4
 and tt2 = TT2
 and tt3 = TT3 tt4
 and tt4 = TT4 tt1
 *)
 
-datatype_new k1 = K11 k2 k3 | K12 k2 k4
+datatype_new (discs_sels) k1 = K11 k2 k3 | K12 k2 k4
 and k2 = K2
 and k3 = K3 k4
 and k4 = K4
 
-datatype_new tt1 = TT11 tt3 tt2 | TT12 tt2 tt4
+datatype_new (discs_sels) tt1 = TT11 tt3 tt2 | TT12 tt2 tt4
 and tt2 = TT2
 and tt3 = TT3 tt1
 and tt4 = TT4
 
 (* SLOW
-datatype_new s1 = S11 s2 s3 s4 | S12 s3 | S13 s2 s6 | S14 s4 s2 | S15 s2 s2
+datatype_new (discs_sels) 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
@@ -154,35 +154,35 @@
 and s8 = S8 nat
 *)
 
-datatype_new 'a deadbar = DeadBar "'a \<Rightarrow> 'a"
-datatype_new 'a deadbar_option = DeadBarOption "'a option \<Rightarrow> 'a option"
-datatype_new ('a, 'b) bar = Bar "'b \<Rightarrow> 'a"
-datatype_new ('a, 'b, 'c, 'd) foo = Foo "'d + 'b \<Rightarrow> 'c + 'a"
-datatype_new 'a deadfoo = DeadFoo "'a \<Rightarrow> 'a + 'a"
+datatype_new (discs_sels) 'a deadbar = DeadBar "'a \<Rightarrow> 'a"
+datatype_new (discs_sels) 'a deadbar_option = DeadBarOption "'a option \<Rightarrow> 'a option"
+datatype_new (discs_sels) ('a, 'b) bar = Bar "'b \<Rightarrow> 'a"
+datatype_new (discs_sels) ('a, 'b, 'c, 'd) foo = Foo "'d + 'b \<Rightarrow> 'c + 'a"
+datatype_new (discs_sels) 'a deadfoo = DeadFoo "'a \<Rightarrow> 'a + 'a"
 
-datatype_new 'a dead_foo = A
-datatype_new ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo"
+datatype_new (discs_sels) 'a dead_foo = A
+datatype_new (discs_sels) ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo"
 
-datatype_new d1 = D
-datatype_new d1' = is_D: D
+datatype_new (discs_sels) d1 = D
+datatype_new (discs_sels) d1' = is_D: D
 
-datatype_new d2 = D nat
-datatype_new d2' = is_D: D nat
+datatype_new (discs_sels) d2 = D nat
+datatype_new (discs_sels) d2' = is_D: D nat
 
-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
+datatype_new (discs_sels) d3 = D | E
+datatype_new (discs_sels) d3' = D | is_E: E
+datatype_new (discs_sels) d3'' = is_D: D | E
+datatype_new (discs_sels) d3''' = is_D: D | 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
+datatype_new (discs_sels) d4 = D nat | E
+datatype_new (discs_sels) d4' = D nat | is_E: E
+datatype_new (discs_sels) d4'' = is_D: D nat | E
+datatype_new (discs_sels) d4''' = is_D: D nat | is_E: E
 
-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
+datatype_new (discs_sels) d5 = D nat | E int
+datatype_new (discs_sels) d5' = D nat | is_E: E int
+datatype_new (discs_sels) d5'' = is_D: D nat | E int
+datatype_new (discs_sels) d5''' = is_D: D nat | is_E: E int
 
 datatype_compat simple
 datatype_compat simple'