support (finite values of) codatatypes in Quickcheck
authorblanchet
Wed Sep 17 08:23:53 2014 +0200 (2014-09-17)
changeset 5835404ac60da613e
parent 58353 c9f374b64d99
child 58355 9a041a55ee95
support (finite values of) codatatypes in Quickcheck
src/HOL/Datatype_Examples/Compat.thy
src/HOL/Library/refute.ML
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/SPARK/Tools/spark_vcs.ML
src/HOL/Statespace/state_fun.ML
src/HOL/Tools/BNF/bnf_lfp_compat.ML
src/HOL/Tools/Quickcheck/exhaustive_generators.ML
src/HOL/Tools/Quickcheck/quickcheck_common.ML
src/HOL/Tools/TFL/casesplit.ML
src/HOL/Tools/TFL/tfl.ML
src/HOL/Tools/TFL/thry.ML
src/HOL/Tools/datatype_realizer.ML
     1.1 --- a/src/HOL/Datatype_Examples/Compat.thy	Tue Sep 16 19:23:37 2014 +0200
     1.2 +++ b/src/HOL/Datatype_Examples/Compat.thy	Wed Sep 17 08:23:53 2014 +0200
     1.3 @@ -5,15 +5,15 @@
     1.4  Tests for compatibility with the old datatype package.
     1.5  *)
     1.6  
     1.7 -header \<open> Tests for Compatibility with the Old Datatype Package \<close>
     1.8 +header {* Tests for Compatibility with the Old Datatype Package *}
     1.9  
    1.10  theory Compat
    1.11  imports Main
    1.12  begin
    1.13  
    1.14 -subsection \<open> Viewing and Registering New-Style Datatypes as Old-Style Ones \<close>
    1.15 +subsection {* Viewing and Registering New-Style Datatypes as Old-Style Ones *}
    1.16  
    1.17 -ML \<open>
    1.18 +ML {*
    1.19  fun check_len n xs label =
    1.20    length xs = n orelse error ("Expected length " ^ string_of_int (length xs) ^ " for " ^ label);
    1.21  
    1.22 @@ -22,22 +22,22 @@
    1.23  
    1.24  fun get_descrs thy lens T_name =
    1.25    (these (Option.map #descr (Old_Datatype_Data.get_info thy T_name)),
    1.26 -   these (Option.map #descr (BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting T_name)),
    1.27 -   these (Option.map #descr (BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Keep_Nesting T_name)))
    1.28 +   these (Option.map #descr (BNF_LFP_Compat.get_info thy [] T_name)),
    1.29 +   these (Option.map #descr (BNF_LFP_Compat.get_info thy [BNF_LFP_Compat.Keep_Nesting] T_name)))
    1.30    |> tap (check_lens lens);
    1.31 -\<close>
    1.32 +*}
    1.33  
    1.34  old_datatype 'a old_lst = Old_Nl | Old_Cns 'a "'a old_lst"
    1.35  
    1.36 -ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name old_lst}; \<close>
    1.37 +ML {* get_descrs @{theory} (1, 1, 1) @{type_name old_lst} *}
    1.38  
    1.39  datatype 'a lst = Nl | Cns 'a "'a lst"
    1.40  
    1.41 -ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name lst}; \<close>
    1.42 +ML {* get_descrs @{theory} (0, 1, 1) @{type_name lst} *}
    1.43  
    1.44  datatype_compat lst
    1.45  
    1.46 -ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name lst}; \<close>
    1.47 +ML {* get_descrs @{theory} (1, 1, 1) @{type_name lst} *}
    1.48  
    1.49  datatype 'b w = W | W' "'b w \<times> 'b list"
    1.50  
    1.51 @@ -45,190 +45,192 @@
    1.52  datatype_compat w
    1.53  *)
    1.54  
    1.55 -ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name w}; \<close>
    1.56 +ML {* get_descrs @{theory} (0, 1, 1) @{type_name w} *}
    1.57  
    1.58  datatype ('c, 'b) s = L 'c | R 'b
    1.59  
    1.60 -ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name s}; \<close>
    1.61 +ML {* get_descrs @{theory} (0, 1, 1) @{type_name s} *}
    1.62  
    1.63  datatype 'd x = X | X' "('d x lst, 'd list) s"
    1.64  
    1.65 -ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name x}; \<close>
    1.66 +ML {* get_descrs @{theory} (0, 1, 1) @{type_name x} *}
    1.67  
    1.68  datatype_compat s
    1.69  
    1.70 -ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name s}; \<close>
    1.71 -ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name x}; \<close>
    1.72 +ML {* get_descrs @{theory} (1, 1, 1) @{type_name s} *}
    1.73 +ML {* get_descrs @{theory} (0, 1, 1) @{type_name x} *}
    1.74  
    1.75  datatype_compat x
    1.76  
    1.77 -ML \<open> get_descrs @{theory} (3, 3, 1) @{type_name x}; \<close>
    1.78 +ML {* get_descrs @{theory} (3, 3, 1) @{type_name x} *}
    1.79  
    1.80  thm x.induct x.rec
    1.81  thm compat_x.induct compat_x.rec
    1.82  
    1.83  datatype 'a tttre = TTTre 'a "'a tttre lst lst lst"
    1.84  
    1.85 -ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name tttre}; \<close>
    1.86 +ML {* get_descrs @{theory} (0, 1, 1) @{type_name tttre} *}
    1.87  
    1.88  datatype_compat tttre
    1.89  
    1.90 -ML \<open> get_descrs @{theory} (4, 4, 1) @{type_name tttre}; \<close>
    1.91 +ML {* get_descrs @{theory} (4, 4, 1) @{type_name tttre} *}
    1.92  
    1.93  thm tttre.induct tttre.rec
    1.94  thm compat_tttre.induct compat_tttre.rec
    1.95  
    1.96  datatype 'a ftre = FEmp | FTre "'a \<Rightarrow> 'a ftre lst"
    1.97  
    1.98 -ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name ftre}; \<close>
    1.99 +ML {* get_descrs @{theory} (0, 1, 1) @{type_name ftre} *}
   1.100  
   1.101  datatype_compat ftre
   1.102  
   1.103 -ML \<open> get_descrs @{theory} (2, 2, 1) @{type_name ftre}; \<close>
   1.104 +ML {* get_descrs @{theory} (2, 2, 1) @{type_name ftre} *}
   1.105  
   1.106  thm ftre.induct ftre.rec
   1.107  thm compat_ftre.induct compat_ftre.rec
   1.108  
   1.109  datatype 'a btre = BTre 'a "'a btre lst" "'a btre lst"
   1.110  
   1.111 -ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name btre}; \<close>
   1.112 +ML {* get_descrs @{theory} (0, 1, 1) @{type_name btre} *}
   1.113  
   1.114  datatype_compat btre
   1.115  
   1.116 -ML \<open> get_descrs @{theory} (3, 3, 1) @{type_name btre}; \<close>
   1.117 +ML {* get_descrs @{theory} (3, 3, 1) @{type_name btre} *}
   1.118  
   1.119  thm btre.induct btre.rec
   1.120  thm compat_btre.induct compat_btre.rec
   1.121  
   1.122  datatype 'a foo = Foo | Foo' 'a "'a bar" and 'a bar = Bar | Bar' 'a "'a foo"
   1.123  
   1.124 -ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name foo}; \<close>
   1.125 -ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name bar}; \<close>
   1.126 +ML {* get_descrs @{theory} (0, 2, 2) @{type_name foo} *}
   1.127 +ML {* get_descrs @{theory} (0, 2, 2) @{type_name bar} *}
   1.128  
   1.129  datatype_compat foo bar
   1.130  
   1.131 -ML \<open> get_descrs @{theory} (2, 2, 2) @{type_name foo}; \<close>
   1.132 -ML \<open> get_descrs @{theory} (2, 2, 2) @{type_name bar}; \<close>
   1.133 +ML {* get_descrs @{theory} (2, 2, 2) @{type_name foo} *}
   1.134 +ML {* get_descrs @{theory} (2, 2, 2) @{type_name bar} *}
   1.135  
   1.136  datatype 'a tre = Tre 'a "'a tre lst"
   1.137  
   1.138 -ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name tre}; \<close>
   1.139 +ML {* get_descrs @{theory} (0, 1, 1) @{type_name tre} *}
   1.140  
   1.141  datatype_compat tre
   1.142  
   1.143 -ML \<open> get_descrs @{theory} (2, 2, 1) @{type_name tre}; \<close>
   1.144 +ML {* get_descrs @{theory} (2, 2, 1) @{type_name tre} *}
   1.145  
   1.146  thm tre.induct tre.rec
   1.147  thm compat_tre.induct compat_tre.rec
   1.148  
   1.149  datatype 'a f = F 'a and 'a g = G 'a
   1.150  
   1.151 -ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name f}; \<close>
   1.152 -ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name g}; \<close>
   1.153 +ML {* get_descrs @{theory} (0, 2, 2) @{type_name f} *}
   1.154 +ML {* get_descrs @{theory} (0, 2, 2) @{type_name g} *}
   1.155  
   1.156  datatype h = H "h f" | H'
   1.157  
   1.158 -ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name h}; \<close>
   1.159 +ML {* get_descrs @{theory} (0, 1, 1) @{type_name h} *}
   1.160  
   1.161  datatype_compat f g
   1.162  
   1.163 -ML \<open> get_descrs @{theory} (2, 2, 2) @{type_name f}; \<close>
   1.164 -ML \<open> get_descrs @{theory} (2, 2, 2) @{type_name g}; \<close>
   1.165 -ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name h}; \<close>
   1.166 +ML {* get_descrs @{theory} (2, 2, 2) @{type_name f} *}
   1.167 +ML {* get_descrs @{theory} (2, 2, 2) @{type_name g} *}
   1.168 +ML {* get_descrs @{theory} (0, 1, 1) @{type_name h} *}
   1.169  
   1.170  datatype_compat h
   1.171  
   1.172 -ML \<open> get_descrs @{theory} (3, 3, 1) @{type_name h}; \<close>
   1.173 +ML {* get_descrs @{theory} (3, 3, 1) @{type_name h} *}
   1.174  
   1.175  thm h.induct h.rec
   1.176  thm compat_h.induct compat_h.rec
   1.177  
   1.178  datatype myunit = MyUnity
   1.179  
   1.180 -ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name myunit}; \<close>
   1.181 +ML {* get_descrs @{theory} (0, 1, 1) @{type_name myunit} *}
   1.182  
   1.183  datatype_compat myunit
   1.184  
   1.185 -ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name myunit}; \<close>
   1.186 +ML {* get_descrs @{theory} (1, 1, 1) @{type_name myunit} *}
   1.187  
   1.188  datatype mylist = MyNil | MyCons nat mylist
   1.189  
   1.190 -ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name mylist}; \<close>
   1.191 +ML {* get_descrs @{theory} (0, 1, 1) @{type_name mylist} *}
   1.192  
   1.193  datatype_compat mylist
   1.194  
   1.195 -ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name mylist}; \<close>
   1.196 +ML {* get_descrs @{theory} (1, 1, 1) @{type_name mylist} *}
   1.197  
   1.198  datatype foo' = FooNil | FooCons bar' foo' and bar' = Bar
   1.199  
   1.200 -ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name foo'}; \<close>
   1.201 -ML \<open> get_descrs @{theory} (0, 2, 2) @{type_name bar'}; \<close>
   1.202 +ML {* get_descrs @{theory} (0, 2, 2) @{type_name foo'} *}
   1.203 +ML {* get_descrs @{theory} (0, 2, 2) @{type_name bar'} *}
   1.204  
   1.205  datatype_compat bar' foo'
   1.206  
   1.207 -ML \<open> get_descrs @{theory} (2, 2, 2) @{type_name foo'}; \<close>
   1.208 -ML \<open> get_descrs @{theory} (2, 2, 2) @{type_name bar'}; \<close>
   1.209 +ML {* get_descrs @{theory} (2, 2, 2) @{type_name foo'} *}
   1.210 +ML {* get_descrs @{theory} (2, 2, 2) @{type_name bar'} *}
   1.211  
   1.212  old_datatype funky = Funky "funky tre" | Funky'
   1.213  
   1.214 -ML \<open> get_descrs @{theory} (3, 3, 3) @{type_name funky}; \<close>
   1.215 +ML {* get_descrs @{theory} (3, 3, 3) @{type_name funky} *}
   1.216  
   1.217  old_datatype fnky = Fnky "nat tre"
   1.218  
   1.219 -ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name fnky}; \<close>
   1.220 +ML {* get_descrs @{theory} (1, 1, 1) @{type_name fnky} *}
   1.221  
   1.222  datatype tree = Tree "tree foo"
   1.223  
   1.224 -ML \<open> get_descrs @{theory} (0, 1, 1) @{type_name tree}; \<close>
   1.225 +ML {* get_descrs @{theory} (0, 1, 1) @{type_name tree} *}
   1.226  
   1.227  datatype_compat tree
   1.228  
   1.229 -ML \<open> get_descrs @{theory} (3, 3, 1) @{type_name tree}; \<close>
   1.230 +ML {* get_descrs @{theory} (3, 3, 1) @{type_name tree} *}
   1.231  
   1.232  thm tree.induct tree.rec
   1.233  thm compat_tree.induct compat_tree.rec
   1.234  
   1.235  
   1.236 -subsection \<open> Creating New-Style Datatypes Using Old-Style Interfaces \<close>
   1.237 +subsection {* Creating New-Style Datatypes Using Old-Style Interfaces *}
   1.238  
   1.239 -ML \<open>
   1.240 +ML {*
   1.241  val l_specs =
   1.242    [((@{binding l}, [("'a", @{sort type})], NoSyn),
   1.243     [(@{binding N}, [], NoSyn),
   1.244 -    (@{binding C}, [@{typ 'a}, Type (Sign.full_name @{theory} @{binding l}, [@{typ 'a}])], NoSyn)])];
   1.245 -\<close>
   1.246 +    (@{binding C}, [@{typ 'a}, Type (Sign.full_name @{theory} @{binding l}, [@{typ 'a}])],
   1.247 +     NoSyn)])];
   1.248 +*}
   1.249  
   1.250 -setup \<open> snd o BNF_LFP_Compat.add_datatype BNF_LFP_Compat.Unfold_Nesting l_specs; \<close>
   1.251 +setup {* snd o BNF_LFP_Compat.add_datatype [] l_specs *}
   1.252  
   1.253 -ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name l}; \<close>
   1.254 +ML {* get_descrs @{theory} (1, 1, 1) @{type_name l} *}
   1.255  
   1.256  thm l.exhaust l.map l.induct l.rec l.size
   1.257  
   1.258 -ML \<open>
   1.259 +ML {*
   1.260  val t_specs =
   1.261    [((@{binding t}, [("'b", @{sort type})], NoSyn),
   1.262 -   [(@{binding T}, [@{typ 'b}, Type (@{type_name l},
   1.263 -       [Type (Sign.full_name @{theory} @{binding t}, [@{typ 'b}])])], NoSyn)])];
   1.264 -\<close>
   1.265 +   [(@{binding T}, [@{typ 'b},
   1.266 +       Type (@{type_name l}, [Type (Sign.full_name @{theory} @{binding t}, [@{typ 'b}])])],
   1.267 +     NoSyn)])];
   1.268 +*}
   1.269  
   1.270 -setup \<open> snd o BNF_LFP_Compat.add_datatype BNF_LFP_Compat.Unfold_Nesting t_specs; \<close>
   1.271 +setup {* snd o BNF_LFP_Compat.add_datatype [] t_specs *}
   1.272  
   1.273 -ML \<open> get_descrs @{theory} (2, 2, 1) @{type_name t}; \<close>
   1.274 +ML {* get_descrs @{theory} (2, 2, 1) @{type_name t} *}
   1.275  
   1.276  thm t.exhaust t.map t.induct t.rec t.size
   1.277  thm compat_t.induct compat_t.rec
   1.278  
   1.279 -ML \<open>
   1.280 +ML {*
   1.281  val ft_specs =
   1.282    [((@{binding ft}, [("'a", @{sort type})], NoSyn),
   1.283     [(@{binding FT0}, [], NoSyn),
   1.284      (@{binding FT}, [@{typ 'a} --> Type (Sign.full_name @{theory} @{binding ft}, [@{typ 'a}])],
   1.285       NoSyn)])];
   1.286 -\<close>
   1.287 +*}
   1.288  
   1.289 -setup \<open> snd o BNF_LFP_Compat.add_datatype BNF_LFP_Compat.Unfold_Nesting ft_specs; \<close>
   1.290 +setup {* snd o BNF_LFP_Compat.add_datatype [] ft_specs *}
   1.291  
   1.292 -ML \<open> get_descrs @{theory} (1, 1, 1) @{type_name ft}; \<close>
   1.293 +ML {* get_descrs @{theory} (1, 1, 1) @{type_name ft} *}
   1.294  
   1.295  thm ft.exhaust ft.induct ft.rec ft.size
   1.296  thm compat_ft.induct compat_ft.rec
     2.1 --- a/src/HOL/Library/refute.ML	Tue Sep 16 19:23:37 2014 +0200
     2.2 +++ b/src/HOL/Library/refute.ML	Wed Sep 17 08:23:53 2014 +0200
     2.3 @@ -416,8 +416,7 @@
     2.4  
     2.5  fun is_IDT_recursor thy (s, _) =
     2.6    let
     2.7 -    val rec_names = Symtab.fold (append o #rec_names o snd)
     2.8 -      (BNF_LFP_Compat.get_all thy BNF_LFP_Compat.Unfold_Nesting) []
     2.9 +    val rec_names = Symtab.fold (append o #rec_names o snd) (BNF_LFP_Compat.get_all thy []) []
    2.10    in
    2.11      (* I'm not quite sure if checking the name 's' is sufficient, *)
    2.12      (* or if we should also check the type 'T'.                   *)
    2.13 @@ -690,7 +689,7 @@
    2.14        (* axiomatic type classes *)
    2.15        | Type (@{type_name itself}, [T1]) => collect_type_axioms T1 axs
    2.16        | Type (s, Ts) =>
    2.17 -        (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s of
    2.18 +        (case BNF_LFP_Compat.get_info thy [] s of
    2.19            SOME _ =>  (* inductive datatype *)
    2.20              (* only collect relevant type axioms for the argument types *)
    2.21              fold collect_type_axioms Ts axs
    2.22 @@ -819,7 +818,7 @@
    2.23        | Type (@{type_name prop}, []) => acc
    2.24        | Type (@{type_name set}, [T1]) => collect_types T1 acc
    2.25        | Type (s, Ts) =>
    2.26 -          (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s of
    2.27 +          (case BNF_LFP_Compat.get_info thy [] s of
    2.28              SOME info =>  (* inductive datatype *)
    2.29                let
    2.30                  val index = #index info
    2.31 @@ -1014,7 +1013,7 @@
    2.32          (* TODO: no warning needed for /positive/ occurrences of IDTs       *)
    2.33          val maybe_spurious = Library.exists (fn
    2.34              Type (s, _) =>
    2.35 -              (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s of
    2.36 +              (case BNF_LFP_Compat.get_info thy [] s of
    2.37                  SOME info =>  (* inductive datatype *)
    2.38                    let
    2.39                      val index           = #index info
    2.40 @@ -1740,7 +1739,7 @@
    2.41      val thy = Proof_Context.theory_of ctxt
    2.42      val (typs, terms) = model
    2.43      fun interpret_term (Type (s, Ts)) =
    2.44 -          (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s of
    2.45 +          (case BNF_LFP_Compat.get_info thy [] s of
    2.46              SOME info =>  (* inductive datatype *)
    2.47                let
    2.48                  (* only recursive IDTs have an associated depth *)
    2.49 @@ -1865,7 +1864,7 @@
    2.50                  HOLogic_empty_set) pairss
    2.51              end
    2.52        | Type (s, Ts) =>
    2.53 -          (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s of
    2.54 +          (case BNF_LFP_Compat.get_info thy [] s of
    2.55              SOME info =>
    2.56                (case AList.lookup (op =) typs T of
    2.57                  SOME 0 =>
    2.58 @@ -1931,7 +1930,7 @@
    2.59            Const (s, T) =>
    2.60              (case body_type T of
    2.61                Type (s', Ts') =>
    2.62 -                (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s' of
    2.63 +                (case BNF_LFP_Compat.get_info thy [] s' of
    2.64                    SOME info =>  (* body type is an inductive datatype *)
    2.65                      let
    2.66                        val index               = #index info
    2.67 @@ -2403,7 +2402,7 @@
    2.68                  end
    2.69                else
    2.70                  NONE  (* not a recursion operator of this datatype *)
    2.71 -          ) (BNF_LFP_Compat.get_all thy BNF_LFP_Compat.Unfold_Nesting) NONE
    2.72 +          ) (BNF_LFP_Compat.get_all thy []) NONE
    2.73      | _ =>  (* head of term is not a constant *)
    2.74        NONE
    2.75    end;
    2.76 @@ -2837,7 +2836,7 @@
    2.77    in
    2.78      (case T of
    2.79        Type (s, Ts) =>
    2.80 -        (case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Unfold_Nesting s of
    2.81 +        (case BNF_LFP_Compat.get_info thy [] s of
    2.82            SOME info =>  (* inductive datatype *)
    2.83              let
    2.84                val (typs, _)           = model
    2.85 @@ -3003,4 +3002,3 @@
    2.86          in thy' end)));
    2.87  
    2.88  end;
    2.89 -
     3.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Tue Sep 16 19:23:37 2014 +0200
     3.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Wed Sep 17 08:23:53 2014 +0200
     3.3 @@ -100,9 +100,9 @@
     3.4      val (_,thy1) = 
     3.5      fold_map (fn ak => fn thy => 
     3.6            let val dt = ((Binding.name ak, [], NoSyn), [(Binding.name ak, [@{typ nat}], NoSyn)])
     3.7 -              val (dt_names, thy1) = BNF_LFP_Compat.add_datatype_dead BNF_LFP_Compat.Unfold_Nesting [dt] thy;
     3.8 +              val (dt_names, thy1) = BNF_LFP_Compat.add_datatype [BNF_LFP_Compat.Kill_Type_Args] [dt] thy;
     3.9              
    3.10 -              val injects = maps (#inject o BNF_LFP_Compat.the_info thy1 BNF_LFP_Compat.Unfold_Nesting) dt_names;
    3.11 +              val injects = maps (#inject o BNF_LFP_Compat.the_info thy1 []) dt_names;
    3.12                val ak_type = Type (Sign.intern_type thy1 ak,[])
    3.13                val ak_sign = Sign.intern_const thy1 ak 
    3.14                
     4.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Tue Sep 16 19:23:37 2014 +0200
     4.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Wed Sep 17 08:23:53 2014 +0200
     4.3 @@ -200,9 +200,9 @@
     4.4  
     4.5      val new_type_names' = map (fn n => n ^ "_Rep") new_type_names;
     4.6  
     4.7 -    val (full_new_type_names',thy1) = BNF_LFP_Compat.add_datatype_dead BNF_LFP_Compat.Unfold_Nesting dts'' thy;
     4.8 +    val (full_new_type_names',thy1) = BNF_LFP_Compat.add_datatype [BNF_LFP_Compat.Kill_Type_Args] dts'' thy;
     4.9  
    4.10 -    val {descr, induct, ...} = BNF_LFP_Compat.the_info thy1 BNF_LFP_Compat.Unfold_Nesting (hd full_new_type_names');
    4.11 +    val {descr, induct, ...} = BNF_LFP_Compat.the_info thy1 [] (hd full_new_type_names');
    4.12      fun nth_dtyp i = Old_Datatype_Aux.typ_of_dtyp descr (Old_Datatype_Aux.DtRec i);
    4.13  
    4.14      val big_name = space_implode "_" new_type_names;
     5.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Tue Sep 16 19:23:37 2014 +0200
     5.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Wed Sep 17 08:23:53 2014 +0200
     5.3 @@ -173,7 +173,7 @@
     5.4  
     5.5  fun add_enum_type tyname tyname' thy =
     5.6    let
     5.7 -    val {case_name, ...} = the (BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Keep_Nesting tyname');
     5.8 +    val {case_name, ...} = the (BNF_LFP_Compat.get_info thy [BNF_LFP_Compat.Keep_Nesting] tyname');
     5.9      val cs = map Const (the (BNF_LFP_Compat.get_constrs thy tyname'));
    5.10      val k = length cs;
    5.11      val T = Type (tyname', []);
    5.12 @@ -210,7 +210,7 @@
    5.13           rtac @{thm subset_antisym} 1 THEN
    5.14           rtac @{thm subsetI} 1 THEN
    5.15           Old_Datatype_Aux.exh_tac (K (#exhaust (BNF_LFP_Compat.the_info
    5.16 -           (Proof_Context.theory_of lthy) BNF_LFP_Compat.Keep_Nesting tyname'))) 1 THEN
    5.17 +           (Proof_Context.theory_of lthy) [BNF_LFP_Compat.Keep_Nesting] tyname'))) 1 THEN
    5.18           ALLGOALS (asm_full_simp_tac lthy));
    5.19  
    5.20      val finite_UNIV = Goal.prove lthy [] []
    5.21 @@ -320,7 +320,7 @@
    5.22                  val tyname = Sign.full_name thy tyb
    5.23                in
    5.24                  (thy |>
    5.25 -                 BNF_LFP_Compat.add_datatype BNF_LFP_Compat.Keep_Nesting
    5.26 +                 BNF_LFP_Compat.add_datatype [BNF_LFP_Compat.Keep_Nesting]
    5.27                     [((tyb, [], NoSyn),
    5.28                       map (fn s => (Binding.name s, [], NoSyn)) els)] |> snd |>
    5.29                   add_enum_type s tyname,
     6.1 --- a/src/HOL/Statespace/state_fun.ML	Tue Sep 16 19:23:37 2014 +0200
     6.2 +++ b/src/HOL/Statespace/state_fun.ML	Wed Sep 17 08:23:53 2014 +0200
     6.3 @@ -338,7 +338,7 @@
     6.4    | mkName (TFree (x,_)) = mkUpper (Long_Name.base_name x)
     6.5    | mkName (TVar ((x,_),_)) = mkUpper (Long_Name.base_name x);
     6.6  
     6.7 -fun is_datatype thy = is_some o BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Keep_Nesting;
     6.8 +fun is_datatype thy = is_some o BNF_LFP_Compat.get_info thy [BNF_LFP_Compat.Keep_Nesting];
     6.9  
    6.10  fun mk_map @{type_name List.list} = Syntax.const @{const_name List.map}
    6.11    | mk_map n = Syntax.const ("StateFun.map_" ^ Long_Name.base_name n);
     7.1 --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Tue Sep 16 19:23:37 2014 +0200
     7.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Wed Sep 17 08:23:53 2014 +0200
     7.3 @@ -10,25 +10,22 @@
     7.4  
     7.5  signature BNF_LFP_COMPAT =
     7.6  sig
     7.7 -  datatype nesting_preference = Keep_Nesting | Unfold_Nesting
     7.8 +  datatype preference = Keep_Nesting | Include_GFPs | Kill_Type_Args
     7.9  
    7.10 -  val get_all: theory -> nesting_preference -> Old_Datatype_Aux.info Symtab.table
    7.11 -  val get_info: theory -> nesting_preference -> string -> Old_Datatype_Aux.info option
    7.12 -  val the_info: theory -> nesting_preference -> string -> Old_Datatype_Aux.info
    7.13 +  val get_all: theory -> preference list -> Old_Datatype_Aux.info Symtab.table
    7.14 +  val get_info: theory -> preference list -> string -> Old_Datatype_Aux.info option
    7.15 +  val the_info: theory -> preference list -> string -> Old_Datatype_Aux.info
    7.16    val the_spec: theory -> string -> (string * sort) list * (string * typ list) list
    7.17 -  val the_descr: theory -> nesting_preference -> string list ->
    7.18 +  val the_descr: theory -> preference list -> string list ->
    7.19      Old_Datatype_Aux.descr * (string * sort) list * string list * string
    7.20      * (string list * string list) * (typ list * typ list)
    7.21    val get_constrs: theory -> string -> (string * typ) list option
    7.22 -  val interpretation: string -> nesting_preference ->
    7.23 +  val interpretation: string -> preference list ->
    7.24      (Old_Datatype_Aux.config -> string list -> theory -> theory) -> theory -> theory
    7.25    val datatype_compat: string list -> local_theory -> local_theory
    7.26    val datatype_compat_global: string list -> theory -> theory
    7.27    val datatype_compat_cmd: string list -> local_theory -> local_theory
    7.28 -  val add_datatype: nesting_preference -> Old_Datatype_Aux.spec list -> theory ->
    7.29 -    string list * theory
    7.30 -  val add_datatype_dead: nesting_preference -> Old_Datatype_Aux.spec list -> theory ->
    7.31 -    string list * theory
    7.32 +  val add_datatype: preference list -> Old_Datatype_Aux.spec list -> theory -> string list * theory
    7.33    val add_primrec: (binding * typ option * mixfix) list -> (Attrib.binding * term) list ->
    7.34     local_theory -> (term list * thm list) * local_theory
    7.35    val add_primrec_global: (binding * typ option * mixfix) list ->
    7.36 @@ -54,7 +51,7 @@
    7.37  val compat_N = "compat_";
    7.38  val rec_split_N = "rec_split_";
    7.39  
    7.40 -datatype nesting_preference = Keep_Nesting | Unfold_Nesting;
    7.41 +datatype preference = Keep_Nesting | Include_GFPs | Kill_Type_Args;
    7.42  
    7.43  fun mk_split_rec_rhs ctxt fpTs Cs (recs as rec1 :: _) =
    7.44    let
    7.45 @@ -206,7 +203,7 @@
    7.46        map (fn (_, (s, Ds, sDss)) => (s, map perm_dtyp Ds, map (apsnd (map perm_dtyp)) sDss)) desc
    7.47    end;
    7.48  
    7.49 -fun mk_infos_of_mutually_recursive_new_datatypes nesting_pref check_names fpT_names0 lthy =
    7.50 +fun mk_infos_of_mutually_recursive_new_datatypes prefs check_names fpT_names0 lthy =
    7.51    let
    7.52      val thy = Proof_Context.theory_of lthy;
    7.53  
    7.54 @@ -214,13 +211,15 @@
    7.55      fun not_mutually_recursive ss =
    7.56        error ("{" ^ commas ss ^ "} is not a complete set of mutually recursive datatypes");
    7.57  
    7.58 -    fun lfp_sugar_of s =
    7.59 +    fun checked_fp_sugar_of s =
    7.60        (case fp_sugar_of lthy s of
    7.61 -        SOME (fp_sugar as {fp = Least_FP, ...}) => fp_sugar
    7.62 -      | _ => not_datatype s);
    7.63 +        SOME (fp_sugar as {fp, ...}) =>
    7.64 +        if member (op =) prefs Include_GFPs orelse fp = Least_FP then fp_sugar else not_datatype s
    7.65 +      | NONE => not_datatype s);
    7.66  
    7.67      val fpTs0 as Type (_, var_As) :: _ =
    7.68 -      map (#T o lfp_sugar_of o fst o dest_Type) (#Ts (#fp_res (lfp_sugar_of (hd fpT_names0))));
    7.69 +      map (#T o checked_fp_sugar_of o fst o dest_Type)
    7.70 +        (#Ts (#fp_res (checked_fp_sugar_of (hd fpT_names0))));
    7.71      val fpT_names = map (fst o dest_Type) fpTs0;
    7.72  
    7.73      val _ = check_names (op =) (fpT_names0, fpT_names) orelse not_mutually_recursive fpT_names0;
    7.74 @@ -237,11 +236,11 @@
    7.75      fun mk_typ_descr index (Type (T_name, Ts)) ({ctrs, ...} : ctr_sugar) =
    7.76        (index, (T_name, map mk_dtyp Ts, map (mk_ctr_descr Ts) ctrs));
    7.77  
    7.78 -    val fp_ctr_sugars = map (#ctr_sugar o lfp_sugar_of) fpT_names;
    7.79 +    val fp_ctr_sugars = map (#ctr_sugar o checked_fp_sugar_of) fpT_names;
    7.80      val orig_descr = map3 mk_typ_descr (0 upto nn_fp - 1) fpTs fp_ctr_sugars;
    7.81      val all_infos = Old_Datatype_Data.get_all thy;
    7.82      val (orig_descr' :: nested_descrs) =
    7.83 -      if nesting_pref = Keep_Nesting then [orig_descr]
    7.84 +      if member (op =) prefs Keep_Nesting then [orig_descr]
    7.85        else fst (Old_Datatype_Aux.unfold_datatypes lthy orig_descr all_infos orig_descr nn_fp);
    7.86  
    7.87      fun cliquify_descr [] = []
    7.88 @@ -269,7 +268,7 @@
    7.89      val fpTs' = Old_Datatype_Aux.get_rec_types descr;
    7.90      val nn = length fpTs';
    7.91  
    7.92 -    val fp_sugars = map (lfp_sugar_of o fst o dest_Type) fpTs';
    7.93 +    val fp_sugars = map (checked_fp_sugar_of o fst o dest_Type) fpTs';
    7.94      val ctr_Tsss = map (map (map (Old_Datatype_Aux.typ_of_dtyp descr) o snd) o #3 o snd) descr;
    7.95      val kkssss = map (map (map body_rec_indices o snd) o #3 o snd) descr;
    7.96  
    7.97 @@ -297,8 +296,8 @@
    7.98      val Xs' = map #X fp_sugars';
    7.99      val ctrXs_Tsss' = map (map (map substAT) o #ctrXs_Tss) fp_sugars';
   7.100      val ctrss' = map2 mk_ctr_of fp_sugars' fpTs';
   7.101 -    val {common_co_inducts = [induct], ...} :: _ = fp_sugars';
   7.102 -    val inducts = map (the_single o #co_inducts) fp_sugars';
   7.103 +    val {common_co_inducts = induct :: _, ...} :: _ = fp_sugars';
   7.104 +    val inducts = map (hd o #co_inducts) fp_sugars';
   7.105      val recs = map #co_rec fp_sugars';
   7.106      val rec_thmss = map #co_rec_thms fp_sugars';
   7.107  
   7.108 @@ -306,14 +305,14 @@
   7.109        | is_nested_rec_type _ = false;
   7.110  
   7.111      val ((lfp_sugar_thms'', (inducts', induct', recs', rec'_thmss)), lthy'') =
   7.112 -      if nesting_pref = Unfold_Nesting andalso
   7.113 -         exists (exists (exists is_nested_rec_type)) ctrXs_Tsss' then
   7.114 +      if member (op =) prefs Keep_Nesting orelse
   7.115 +         not (exists (exists (exists is_nested_rec_type)) ctrXs_Tsss') then
   7.116 +        ((lfp_sugar_thms', (inducts, induct, recs, rec_thmss)), lthy')
   7.117 +      else
   7.118          define_split_rec_derive_induct_rec_thms Xs' fpTs' ctrXs_Tsss' ctrss' inducts induct recs
   7.119            rec_thmss lthy'
   7.120          |>> `(fn (inducts', induct', _, rec'_thmss) =>
   7.121 -          SOME ((inducts', induct', mk_induct_attrs ctrss'), (rec'_thmss, [])))
   7.122 -      else
   7.123 -        ((lfp_sugar_thms', (inducts, induct, recs, rec_thmss)), lthy');
   7.124 +          SOME ((inducts', induct', mk_induct_attrs ctrss'), (rec'_thmss, [])));
   7.125  
   7.126      val rec'_names = map (fst o dest_Const) recs';
   7.127      val rec'_thms = flat rec'_thmss;
   7.128 @@ -332,53 +331,58 @@
   7.129      (nn, b_names, compat_b_names, lfp_sugar_thms'', infos, lthy'')
   7.130    end;
   7.131  
   7.132 -fun infos_of_new_datatype_mutual_cluster lthy fpT_name =
   7.133 -  #5 (mk_infos_of_mutually_recursive_new_datatypes Keep_Nesting subset [fpT_name] lthy)
   7.134 +fun infos_of_new_datatype_mutual_cluster lthy prefs fpT_name =
   7.135 +  #5 (mk_infos_of_mutually_recursive_new_datatypes prefs subset [fpT_name] lthy)
   7.136    handle ERROR _ => [];
   7.137  
   7.138 -fun get_all thy nesting_pref =
   7.139 +fun get_all thy prefs =
   7.140    let
   7.141      val lthy = Proof_Context.init_global thy;
   7.142      val old_info_tab = Old_Datatype_Data.get_all thy;
   7.143      val new_T_names = BNF_FP_Def_Sugar.fp_sugars_of_global thy
   7.144        |> map_filter (try (fn {T = Type (s, _), fp_res_index = 0, ...} => s));
   7.145 -    val new_infos = maps (infos_of_new_datatype_mutual_cluster lthy) new_T_names;
   7.146 +    val new_infos =
   7.147 +      maps (infos_of_new_datatype_mutual_cluster lthy (insert (op =) Keep_Nesting prefs))
   7.148 +        new_T_names;
   7.149    in
   7.150 -    fold (if nesting_pref = Keep_Nesting then Symtab.update else Symtab.default) new_infos
   7.151 +    fold (if member (op =) prefs Keep_Nesting then Symtab.update else Symtab.default) new_infos
   7.152        old_info_tab
   7.153    end;
   7.154  
   7.155 -fun get_one get_old get_new thy nesting_pref x =
   7.156 -  let val (get_fst, get_snd) = (get_old thy, get_new thy) |> nesting_pref = Keep_Nesting ? swap in
   7.157 +fun get_one get_old get_new thy prefs x =
   7.158 +  let
   7.159 +    val (get_fst, get_snd) = (get_old thy, get_new thy) |> member (op =) prefs Keep_Nesting ? swap;
   7.160 +  in
   7.161      (case get_fst x of NONE => get_snd x | res => res)
   7.162    end;
   7.163  
   7.164 -fun get_info_of_new_datatype thy T_name =
   7.165 +fun get_info_of_new_datatype prefs thy T_name =
   7.166    let val lthy = Proof_Context.init_global thy in
   7.167 -    AList.lookup (op =) (infos_of_new_datatype_mutual_cluster lthy T_name) T_name
   7.168 +    AList.lookup (op =) (infos_of_new_datatype_mutual_cluster lthy prefs T_name) T_name
   7.169    end;
   7.170  
   7.171 -val get_info = get_one Old_Datatype_Data.get_info get_info_of_new_datatype;
   7.172 +fun get_info thy prefs =
   7.173 +  get_one Old_Datatype_Data.get_info (get_info_of_new_datatype prefs) thy prefs;
   7.174  
   7.175 -fun the_info thy nesting_pref T_name =
   7.176 -  (case get_info thy nesting_pref T_name of
   7.177 +fun the_info thy prefs T_name =
   7.178 +  (case get_info thy prefs T_name of
   7.179      SOME info => info
   7.180    | NONE => error ("Unknown datatype " ^ quote T_name));
   7.181  
   7.182  fun the_spec thy T_name =
   7.183    let
   7.184 -    val {descr, index, ...} = the_info thy Keep_Nesting T_name;
   7.185 +    val {descr, index, ...} = the_info thy [Keep_Nesting, Include_GFPs] T_name;
   7.186      val (_, Ds, ctrs0) = the (AList.lookup (op =) descr index);
   7.187      val tfrees = map Old_Datatype_Aux.dest_DtTFree Ds;
   7.188      val ctrs = map (apsnd (map (Old_Datatype_Aux.typ_of_dtyp descr))) ctrs0;
   7.189    in (tfrees, ctrs) end;
   7.190  
   7.191 -fun the_descr thy nesting_pref (T_names0 as T_name01 :: _) =
   7.192 +fun the_descr thy prefs (T_names0 as T_name01 :: _) =
   7.193    let
   7.194      fun not_mutually_recursive ss =
   7.195        error ("{" ^ commas ss ^ "} is not a complete set of mutually recursive datatypes");
   7.196  
   7.197 -    val info = the_info thy nesting_pref T_name01;
   7.198 +    val info = the_info thy prefs T_name01;
   7.199      val descr = #descr info;
   7.200  
   7.201      val (_, Ds, _) = the (AList.lookup (op =) descr (#index info));
   7.202 @@ -420,25 +424,26 @@
   7.203        map (apsnd mk_ctr_typ) ctrs
   7.204      end);
   7.205  
   7.206 -fun old_interpretation_of nesting_pref f config T_names thy =
   7.207 -  if nesting_pref = Unfold_Nesting orelse exists (is_none o fp_sugar_of_global thy) T_names then
   7.208 +fun old_interpretation_of prefs f config T_names thy =
   7.209 +  if not (member (op =) prefs Keep_Nesting) orelse
   7.210 +     exists (is_none o fp_sugar_of_global thy) T_names then
   7.211      f config T_names thy
   7.212    else
   7.213      thy;
   7.214  
   7.215 -fun new_interpretation_of nesting_pref f (fp_sugars : fp_sugar list) thy =
   7.216 +fun new_interpretation_of prefs f (fp_sugars : fp_sugar list) thy =
   7.217    let val T_names = map (fst o dest_Type o #T) fp_sugars in
   7.218 -    if forall (curry (op =) Least_FP o #fp) fp_sugars andalso
   7.219 -        (nesting_pref = Keep_Nesting orelse
   7.220 +    if (member (op =) prefs Include_GFPs orelse forall (curry (op =) Least_FP o #fp) fp_sugars)
   7.221 +       andalso (member (op =) prefs Keep_Nesting orelse
   7.222           exists (is_none o Old_Datatype_Data.get_info thy) T_names) then
   7.223        f Old_Datatype_Aux.default_config T_names thy
   7.224      else
   7.225        thy
   7.226    end;
   7.227  
   7.228 -fun interpretation name nesting_pref f =
   7.229 -  let val new_f = new_interpretation_of nesting_pref f in
   7.230 -    Old_Datatype_Data.interpretation (old_interpretation_of nesting_pref f)
   7.231 +fun interpretation name prefs f =
   7.232 +  let val new_f = new_interpretation_of prefs f in
   7.233 +    Old_Datatype_Data.interpretation (old_interpretation_of prefs f)
   7.234      #> fp_sugars_interpretation name new_f (Local_Theory.background_theory o new_f)
   7.235    end;
   7.236  
   7.237 @@ -447,7 +452,7 @@
   7.238  fun datatype_compat fpT_names lthy =
   7.239    let
   7.240      val (nn, b_names, compat_b_names, lfp_sugar_thms, infos, lthy') =
   7.241 -      mk_infos_of_mutually_recursive_new_datatypes Unfold_Nesting eq_set fpT_names lthy;
   7.242 +      mk_infos_of_mutually_recursive_new_datatypes [] eq_set fpT_names lthy;
   7.243  
   7.244      val all_notes =
   7.245        (case lfp_sugar_thms of
   7.246 @@ -498,12 +503,13 @@
   7.247      datatype_compat fpT_names lthy
   7.248    end;
   7.249  
   7.250 -fun gen_add_datatype live nesting_pref old_specs thy =
   7.251 +fun add_datatype prefs old_specs thy =
   7.252    let
   7.253      val fpT_names = map (Sign.full_name thy o #1 o fst) old_specs;
   7.254  
   7.255      fun new_type_args_of (s, S) =
   7.256 -      (if live then SOME Binding.empty else NONE, (TFree (s, @{sort type}), S));
   7.257 +      (if member (op =) prefs Kill_Type_Args then NONE else SOME Binding.empty,
   7.258 +       (TFree (s, @{sort type}), S));
   7.259      fun new_ctr_spec_of (b, Ts, mx) = (((Binding.empty, b), map (pair Binding.empty) Ts), mx);
   7.260  
   7.261      fun new_spec_of ((b, old_tyargs, mx), old_ctr_specs) =
   7.262 @@ -515,12 +521,9 @@
   7.263      (fpT_names,
   7.264       thy
   7.265       |> map_local_theory (co_datatypes Least_FP construct_lfp (default_ctr_options, new_specs))
   7.266 -     |> nesting_pref = Unfold_Nesting ? perhaps (try (datatype_compat_global fpT_names)))
   7.267 +     |> not (member (op =) prefs Keep_Nesting) ? perhaps (try (datatype_compat_global fpT_names)))
   7.268    end;
   7.269  
   7.270 -val add_datatype = gen_add_datatype true;
   7.271 -val add_datatype_dead = gen_add_datatype false;
   7.272 -
   7.273  val add_primrec = apfst (apsnd flat) ooo BNF_LFP_Rec_Sugar.add_primrec;
   7.274  val add_primrec_global = apfst (apsnd flat) ooo BNF_LFP_Rec_Sugar.add_primrec_global;
   7.275  val add_primrec_overloaded = apfst (apsnd flat) oooo BNF_LFP_Rec_Sugar.add_primrec_overloaded;
     8.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Tue Sep 16 19:23:37 2014 +0200
     8.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Wed Sep 17 08:23:53 2014 +0200
     8.3 @@ -263,7 +263,8 @@
     8.4    let
     8.5      val cnstrs = flat (maps
     8.6        (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
     8.7 -      (Symtab.dest (BNF_LFP_Compat.get_all (Proof_Context.theory_of ctxt) BNF_LFP_Compat.Keep_Nesting)))
     8.8 +      (Symtab.dest (BNF_LFP_Compat.get_all (Proof_Context.theory_of ctxt)
     8.9 +         Quickcheck_Common.compat_prefs)))
    8.10      fun is_constrt (Const (s, T), ts) = (case (AList.lookup (op =) cnstrs s, body_type T) of
    8.11          (SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname'
    8.12        | _ => false)
    8.13 @@ -547,10 +548,11 @@
    8.14      (@{sort exhaustive}, instantiate_exhaustive_datatype)
    8.15  
    8.16  val setup_bounded_forall_datatype_interpretation =
    8.17 -  BNF_LFP_Compat.interpretation bounded_forall_plugin BNF_LFP_Compat.Keep_Nesting
    8.18 +  BNF_LFP_Compat.interpretation bounded_forall_plugin Quickcheck_Common.compat_prefs
    8.19      (Quickcheck_Common.ensure_sort
    8.20         (((@{sort type}, @{sort type}), @{sort bounded_forall}),
    8.21 -       (fn thy => BNF_LFP_Compat.the_descr thy BNF_LFP_Compat.Keep_Nesting, instantiate_bounded_forall_datatype)))
    8.22 +       (fn thy => BNF_LFP_Compat.the_descr thy Quickcheck_Common.compat_prefs,
    8.23 +        instantiate_bounded_forall_datatype)))
    8.24  
    8.25  val active = Attrib.setup_config_bool @{binding quickcheck_exhaustive_active} (K true);
    8.26  
     9.1 --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Tue Sep 16 19:23:37 2014 +0200
     9.2 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Wed Sep 17 08:23:53 2014 +0200
     9.3 @@ -6,6 +6,7 @@
     9.4  
     9.5  signature QUICKCHECK_COMMON =
     9.6  sig
     9.7 +  val compat_prefs : BNF_LFP_Compat.preference list
     9.8    val strip_imp : term -> (term list * term)
     9.9    val reflect_bool : bool -> term
    9.10    val define_functions : ((term list -> term list) * (Proof.context -> tactic) option)
    9.11 @@ -46,6 +47,8 @@
    9.12  
    9.13  (* static options *)
    9.14  
    9.15 +val compat_prefs = [BNF_LFP_Compat.Keep_Nesting, BNF_LFP_Compat.Include_GFPs]
    9.16 +
    9.17  val define_foundationally = false
    9.18  
    9.19  (* HOLogic's term functions *)
    9.20 @@ -420,10 +423,10 @@
    9.21  
    9.22  fun ensure_common_sort_datatype (sort, instantiate) =
    9.23    ensure_sort (((@{sort typerep}, @{sort term_of}), sort),
    9.24 -    (fn thy => BNF_LFP_Compat.the_descr thy BNF_LFP_Compat.Keep_Nesting, instantiate))
    9.25 +    (fn thy => BNF_LFP_Compat.the_descr thy compat_prefs, instantiate))
    9.26  
    9.27  fun datatype_interpretation name =
    9.28 -  BNF_LFP_Compat.interpretation name BNF_LFP_Compat.Keep_Nesting o ensure_common_sort_datatype
    9.29 +  BNF_LFP_Compat.interpretation name compat_prefs o ensure_common_sort_datatype
    9.30    
    9.31  (** generic parametric compilation **)
    9.32  
    10.1 --- a/src/HOL/Tools/TFL/casesplit.ML	Tue Sep 16 19:23:37 2014 +0200
    10.2 +++ b/src/HOL/Tools/TFL/casesplit.ML	Wed Sep 17 08:23:53 2014 +0200
    10.3 @@ -24,7 +24,7 @@
    10.4                       Type(ty_str, _) => ty_str
    10.5                     | TFree(s,_)  => error ("Free type: " ^ s)
    10.6                     | TVar((s,i),_) => error ("Free variable: " ^ s)
    10.7 -      val {induct, ...} = BNF_LFP_Compat.the_info thy BNF_LFP_Compat.Keep_Nesting ty_str
    10.8 +      val {induct, ...} = BNF_LFP_Compat.the_info thy [BNF_LFP_Compat.Keep_Nesting] ty_str
    10.9      in
   10.10        cases_thm_of_induct_thm induct
   10.11      end;
    11.1 --- a/src/HOL/Tools/TFL/tfl.ML	Tue Sep 16 19:23:37 2014 +0200
    11.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Wed Sep 17 08:23:53 2014 +0200
    11.3 @@ -435,7 +435,7 @@
    11.4         put_simpset HOL_basic_ss ctxt
    11.5            addsimps case_rewrites
    11.6            |> fold (Simplifier.add_cong o #case_cong_weak o snd)
    11.7 -              (Symtab.dest (BNF_LFP_Compat.get_all theory BNF_LFP_Compat.Keep_Nesting))
    11.8 +              (Symtab.dest (BNF_LFP_Compat.get_all theory [BNF_LFP_Compat.Keep_Nesting]))
    11.9       val corollaries' = map (Simplifier.simplify case_simpset) corollaries
   11.10       val extract = Rules.CONTEXT_REWRITE_RULE
   11.11                       (f, [R], @{thm cut_apply}, meta_tflCongs @ context_congs)
    12.1 --- a/src/HOL/Tools/TFL/thry.ML	Tue Sep 16 19:23:37 2014 +0200
    12.2 +++ b/src/HOL/Tools/TFL/thry.ML	Wed Sep 17 08:23:53 2014 +0200
    12.3 @@ -58,20 +58,20 @@
    12.4   *---------------------------------------------------------------------------*)
    12.5  
    12.6  fun match_info thy dtco =
    12.7 -  case (BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Keep_Nesting dtco,
    12.8 +  case (BNF_LFP_Compat.get_info thy [BNF_LFP_Compat.Keep_Nesting] dtco,
    12.9           BNF_LFP_Compat.get_constrs thy dtco) of
   12.10        (SOME {case_name, ... }, SOME constructors) =>
   12.11          SOME {case_const = Const (case_name, Sign.the_const_type thy case_name), constructors = map Const constructors}
   12.12      | _ => NONE;
   12.13  
   12.14 -fun induct_info thy dtco = case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Keep_Nesting dtco of
   12.15 +fun induct_info thy dtco = case BNF_LFP_Compat.get_info thy [BNF_LFP_Compat.Keep_Nesting] dtco of
   12.16          NONE => NONE
   12.17        | SOME {nchotomy, ...} =>
   12.18            SOME {nchotomy = nchotomy,
   12.19                  constructors = (map Const o the o BNF_LFP_Compat.get_constrs thy) dtco};
   12.20  
   12.21  fun extract_info thy =
   12.22 - let val infos = map snd (Symtab.dest (BNF_LFP_Compat.get_all thy BNF_LFP_Compat.Keep_Nesting))
   12.23 + let val infos = map snd (Symtab.dest (BNF_LFP_Compat.get_all thy [BNF_LFP_Compat.Keep_Nesting]))
   12.24   in {case_congs = map (mk_meta_eq o #case_cong) infos,
   12.25       case_rewrites = maps (map mk_meta_eq o #case_rewrites) infos}
   12.26   end;
    13.1 --- a/src/HOL/Tools/datatype_realizer.ML	Tue Sep 16 19:23:37 2014 +0200
    13.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Wed Sep 17 08:23:53 2014 +0200
    13.3 @@ -233,7 +233,7 @@
    13.4    else
    13.5      let
    13.6        val _ = Old_Datatype_Aux.message config "Adding realizers for induction and case analysis ...";
    13.7 -      val infos = map (BNF_LFP_Compat.the_info thy BNF_LFP_Compat.Unfold_Nesting) names;
    13.8 +      val infos = map (BNF_LFP_Compat.the_info thy []) names;
    13.9        val info :: _ = infos;
   13.10      in
   13.11        thy
   13.12 @@ -241,7 +241,6 @@
   13.13        |> fold_rev (perhaps o try o make_casedists) infos
   13.14      end;
   13.15  
   13.16 -val _ = Theory.setup (BNF_LFP_Compat.interpretation extraction_plugin BNF_LFP_Compat.Unfold_Nesting
   13.17 -  add_dt_realizers);
   13.18 +val _ = Theory.setup (BNF_LFP_Compat.interpretation extraction_plugin [] add_dt_realizers);
   13.19  
   13.20  end;