--- a/src/HOL/BNF_Examples/ListF.thy Fri May 30 12:27:51 2014 +0200
+++ b/src/HOL/BNF_Examples/ListF.thy Fri May 30 12:27:51 2014 +0200
@@ -14,6 +14,7 @@
datatype_new 'a listF (map: mapF rel: relF) =
NilF (defaults tlF: NilF) | Conss (hdF: 'a) (tlF: "'a listF")
+
datatype_compat listF
definition Singll ("[[_]]") where
--- a/src/HOL/List.thy Fri May 30 12:27:51 2014 +0200
+++ b/src/HOL/List.thy Fri May 30 12:27:51 2014 +0200
@@ -8,9 +8,10 @@
imports Presburger Code_Numeral Quotient Lifting_Set Lifting_Option Lifting_Product
begin
-datatype_new (set: 'a) list (map: map rel: list_all2) =
+datatype_new (set: 'a) list (map: map rel: list_all2) =
Nil (defaults tl: "[]") ("[]")
| Cons (hd: 'a) (tl: "'a list") (infixr "#" 65)
+
datatype_compat list
lemma [case_names Nil Cons, cases type: list]:
--- a/src/HOL/Option.thy Fri May 30 12:27:51 2014 +0200
+++ b/src/HOL/Option.thy Fri May 30 12:27:51 2014 +0200
@@ -11,6 +11,7 @@
datatype_new 'a option =
None
| Some (the: 'a)
+
datatype_compat option
lemma [case_names None Some, cases type: option]: