# HG changeset patch
# User haftmann
# Date 1245163027 -7200
# Node ID a616e56a5ec8f3065e4239e7d8230c03123d5a0d
# Parent  cc969090c204e9d5c750687a31326e9a8228b2ba
datatype packages: record datatype_config for configuration flags; less verbose signatures

diff -r cc969090c204 -r a616e56a5ec8 src/HOL/Tools/datatype_package/datatype_abs_proofs.ML
--- a/src/HOL/Tools/datatype_package/datatype_abs_proofs.ML	Tue Jun 16 16:36:56 2009 +0200
+++ b/src/HOL/Tools/datatype_package/datatype_abs_proofs.ML	Tue Jun 16 16:37:07 2009 +0200
@@ -14,26 +14,29 @@
 
 signature DATATYPE_ABS_PROOFS =
 sig
-  val prove_casedist_thms : string list ->
-    DatatypeAux.descr list -> (string * sort) list -> thm ->
+  type datatype_config = DatatypeAux.datatype_config
+  type descr = DatatypeAux.descr
+  type datatype_info = DatatypeAux.datatype_info
+  val prove_casedist_thms : datatype_config -> string list ->
+    descr list -> (string * sort) list -> thm ->
     attribute list -> theory -> thm list * theory
-  val prove_primrec_thms : bool -> string list ->
-    DatatypeAux.descr list -> (string * sort) list ->
-      DatatypeAux.datatype_info Symtab.table -> thm list list -> thm list list ->
+  val prove_primrec_thms : datatype_config -> string list ->
+    descr list -> (string * sort) list ->
+      datatype_info Symtab.table -> thm list list -> thm list list ->
         simpset -> thm -> theory -> (string list * thm list) * theory
-  val prove_case_thms : bool -> string list ->
-    DatatypeAux.descr list -> (string * sort) list ->
+  val prove_case_thms : datatype_config -> string list ->
+    descr list -> (string * sort) list ->
       string list -> thm list -> theory -> (thm list list * string list) * theory
-  val prove_split_thms : string list ->
-    DatatypeAux.descr list -> (string * sort) list ->
+  val prove_split_thms : datatype_config -> string list ->
+    descr list -> (string * sort) list ->
       thm list list -> thm list list -> thm list -> thm list list -> theory ->
         (thm * thm) list * theory
-  val prove_nchotomys : string list -> DatatypeAux.descr list ->
+  val prove_nchotomys : datatype_config -> string list -> descr list ->
     (string * sort) list -> thm list -> theory -> thm list * theory
-  val prove_weak_case_congs : string list -> DatatypeAux.descr list ->
+  val prove_weak_case_congs : string list -> descr list ->
     (string * sort) list -> theory -> thm list * theory
   val prove_case_congs : string list ->
-    DatatypeAux.descr list -> (string * sort) list ->
+    descr list -> (string * sort) list ->
       thm list -> thm list list -> theory -> thm list * theory
 end;
 
@@ -44,9 +47,9 @@
 
 (************************ case distinction theorems ***************************)
 
-fun prove_casedist_thms new_type_names descr sorts induct case_names_exhausts thy =
+fun prove_casedist_thms (config : datatype_config) new_type_names descr sorts induct case_names_exhausts thy =
   let
-    val _ = message "Proving case distinction theorems ...";
+    val _ = message config "Proving case distinction theorems ...";
 
     val descr' = List.concat descr;
     val recTs = get_rec_types descr' sorts;
@@ -86,13 +89,13 @@
 
 (*************************** primrec combinators ******************************)
 
-fun prove_primrec_thms flat_names new_type_names descr sorts
+fun prove_primrec_thms (config : datatype_config) new_type_names descr sorts
     (dt_info : datatype_info Symtab.table) constr_inject dist_rewrites dist_ss induct thy =
   let
-    val _ = message "Constructing primrec combinators ...";
+    val _ = message config "Constructing primrec combinators ...";
 
     val big_name = space_implode "_" new_type_names;
-    val thy0 = add_path flat_names big_name thy;
+    val thy0 = add_path (#flat_names config) big_name thy;
 
     val descr' = List.concat descr;
     val recTs = get_rec_types descr' sorts;
@@ -153,7 +156,7 @@
 
     val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
         InductivePackage.add_inductive_global (serial_string ())
-          {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
+          {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
             alt_name = Binding.name big_rec_name', coind = false, no_elim = false, no_ind = true,
             skip_mono = true, fork_mono = false}
           (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
@@ -162,7 +165,7 @@
 
     (* prove uniqueness and termination of primrec combinators *)
 
-    val _ = message "Proving termination and uniqueness of primrec functions ...";
+    val _ = message config "Proving termination and uniqueness of primrec functions ...";
 
     fun mk_unique_tac ((tac, intrs), ((((i, (tname, _, constrs)), elim), T), T')) =
       let
@@ -242,13 +245,13 @@
            Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
              set $ Free ("x", T) $ Free ("y", T'))))))
                (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts))
-      ||> parent_path flat_names
+      ||> parent_path (#flat_names config) 
       ||> Theory.checkpoint;
 
 
     (* prove characteristic equations for primrec combinators *)
 
-    val _ = message "Proving characteristic theorems for primrec combinators ..."
+    val _ = message config "Proving characteristic theorems for primrec combinators ..."
 
     val rec_thms = map (fn t => SkipProof.prove_global thy2 [] [] t
       (fn _ => EVERY
@@ -272,11 +275,11 @@
 
 (***************************** case combinators *******************************)
 
-fun prove_case_thms flat_names new_type_names descr sorts reccomb_names primrec_thms thy =
+fun prove_case_thms (config : datatype_config) new_type_names descr sorts reccomb_names primrec_thms thy =
   let
-    val _ = message "Proving characteristic theorems for case combinators ...";
+    val _ = message config "Proving characteristic theorems for case combinators ...";
 
-    val thy1 = add_path flat_names (space_implode "_" new_type_names) thy;
+    val thy1 = add_path (#flat_names config) (space_implode "_" new_type_names) thy;
 
     val descr' = List.concat descr;
     val recTs = get_rec_types descr' sorts;
@@ -338,7 +341,7 @@
     thy2
     |> Context.the_theory o fold (fold Nitpick_Const_Simp_Thms.add_thm) case_thms
        o Context.Theory
-    |> parent_path flat_names
+    |> parent_path (#flat_names config)
     |> store_thmss "cases" new_type_names case_thms
     |-> (fn thmss => pair (thmss, case_names))
   end;
@@ -346,12 +349,12 @@
 
 (******************************* case splitting *******************************)
 
-fun prove_split_thms new_type_names descr sorts constr_inject dist_rewrites
+fun prove_split_thms (config : datatype_config) new_type_names descr sorts constr_inject dist_rewrites
     casedist_thms case_thms thy =
   let
-    val _ = message "Proving equations for case splitting ...";
+    val _ = message config "Proving equations for case splitting ...";
 
-    val descr' = List.concat descr;
+    val descr' = flat descr;
     val recTs = get_rec_types descr' sorts;
     val newTs = Library.take (length (hd descr), recTs);
 
@@ -395,9 +398,9 @@
 
 (************************* additional theorems for TFL ************************)
 
-fun prove_nchotomys new_type_names descr sorts casedist_thms thy =
+fun prove_nchotomys (config : datatype_config) new_type_names descr sorts casedist_thms thy =
   let
-    val _ = message "Proving additional theorems for TFL ...";
+    val _ = message config "Proving additional theorems for TFL ...";
 
     fun prove_nchotomy (t, exhaustion) =
       let
diff -r cc969090c204 -r a616e56a5ec8 src/HOL/Tools/datatype_package/datatype_aux.ML
--- a/src/HOL/Tools/datatype_package/datatype_aux.ML	Tue Jun 16 16:36:56 2009 +0200
+++ b/src/HOL/Tools/datatype_package/datatype_aux.ML	Tue Jun 16 16:37:07 2009 +0200
@@ -6,8 +6,9 @@
 
 signature DATATYPE_AUX =
 sig
-  val quiet_mode : bool ref
-  val message : string -> unit
+  type datatype_config
+  val default_datatype_config : datatype_config
+  val message : datatype_config -> string -> unit
   
   val add_path : bool -> string -> theory -> theory
   val parent_path : bool -> theory -> theory
@@ -67,8 +68,13 @@
 structure DatatypeAux : DATATYPE_AUX =
 struct
 
-val quiet_mode = ref false;
-fun message s = if !quiet_mode then () else writeln s;
+(* datatype option flags *)
+
+type datatype_config = { strict: bool, flat_names: bool, quiet: bool };
+val default_datatype_config : datatype_config =
+  { strict = true, flat_names = false, quiet = false };
+fun message ({ quiet, ...} : datatype_config) s =
+  if quiet then () else writeln s;
 
 fun add_path flat_names s = if flat_names then I else Sign.add_path s;
 fun parent_path flat_names = if flat_names then I else Sign.parent_path;
diff -r cc969090c204 -r a616e56a5ec8 src/HOL/Tools/datatype_package/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_package/datatype_codegen.ML	Tue Jun 16 16:36:56 2009 +0200
+++ b/src/HOL/Tools/datatype_package/datatype_codegen.ML	Tue Jun 16 16:37:07 2009 +0200
@@ -426,7 +426,7 @@
 
 (* register a datatype etc. *)
 
-fun add_all_code dtcos thy =
+fun add_all_code config dtcos thy =
   let
     val (vs :: _, coss) = (split_list o map (DatatypePackage.the_datatype_spec thy)) dtcos;
     val any_css = map2 (mk_constr_consts thy vs) dtcos coss;
@@ -437,7 +437,7 @@
   in
     if null css then thy
     else thy
-      |> tap (fn _ => DatatypeAux.message "Registering datatype for code generator ...")
+      |> tap (fn _ => DatatypeAux.message config "Registering datatype for code generator ...")
       |> fold Code.add_datatype css
       |> fold_rev Code.add_default_eqn case_rewrites
       |> fold Code.add_case certs
diff -r cc969090c204 -r a616e56a5ec8 src/HOL/Tools/datatype_package/datatype_package.ML
--- a/src/HOL/Tools/datatype_package/datatype_package.ML	Tue Jun 16 16:36:56 2009 +0200
+++ b/src/HOL/Tools/datatype_package/datatype_package.ML	Tue Jun 16 16:37:07 2009 +0200
@@ -6,6 +6,7 @@
 
 signature DATATYPE_PACKAGE =
 sig
+  type datatype_config = DatatypeAux.datatype_config
   type datatype_info = DatatypeAux.datatype_info
   type descr = DatatypeAux.descr
   val get_datatypes : theory -> datatype_info Symtab.table
@@ -24,39 +25,23 @@
   val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option
   val read_typ: theory ->
     (typ list * (string * sort) list) * string -> typ list * (string * sort) list
-  val interpretation : (string list -> theory -> theory) -> theory -> theory
-  val rep_datatype : ({distinct : thm list list,
-       inject : thm list list,
-       exhaustion : thm list,
-       rec_thms : thm list,
-       case_thms : thm list list,
-       split_thms : (thm * thm) list,
-       induction : thm,
-       simps : thm list} -> Proof.context -> Proof.context) -> string list option -> term list
-    -> theory -> Proof.state;
-  val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state;
-  val add_datatype : bool -> bool -> string list -> (string list * binding * mixfix *
-    (binding * typ list * mixfix) list) list -> theory ->
-      {distinct : thm list list,
-       inject : thm list list,
-       exhaustion : thm list,
-       rec_thms : thm list,
-       case_thms : thm list list,
-       split_thms : (thm * thm) list,
-       induction : thm,
-       simps : thm list} * theory
-  val add_datatype_cmd : bool -> string list -> (string list * binding * mixfix *
-    (binding * string list * mixfix) list) list -> theory ->
-      {distinct : thm list list,
-       inject : thm list list,
-       exhaustion : thm list,
-       rec_thms : thm list,
-       case_thms : thm list list,
-       split_thms : (thm * thm) list,
-       induction : thm,
-       simps : thm list} * theory
+  val interpretation : (datatype_config -> string list -> theory -> theory) -> theory -> theory
+  type rules = {distinct : thm list list,
+    inject : thm list list,
+    exhaustion : thm list,
+    rec_thms : thm list,
+    case_thms : thm list list,
+    split_thms : (thm * thm) list,
+    induction : thm,
+    simps : thm list}
+  val rep_datatype : datatype_config -> (rules -> Proof.context -> Proof.context)
+    -> string list option -> term list -> theory -> Proof.state;
+  val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state
+  val add_datatype : datatype_config -> string list -> (string list * binding * mixfix *
+    (binding * typ list * mixfix) list) list -> theory -> rules * theory
+  val add_datatype_cmd : string list -> (string list * binding * mixfix *
+    (binding * string list * mixfix) list) list -> theory -> rules * theory
   val setup: theory -> theory
-  val quiet_mode : bool ref
   val print_datatypes : theory -> unit
 end;
 
@@ -65,8 +50,6 @@
 
 open DatatypeAux;
 
-val quiet_mode = quiet_mode;
-
 
 (* theory data *)
 
@@ -358,31 +341,41 @@
     case_cong = case_cong,
     weak_case_cong = weak_case_cong});
 
-structure DatatypeInterpretation = InterpretationFun(type T = string list val eq = op =);
-val interpretation = DatatypeInterpretation.interpretation;
+type rules = {distinct : thm list list,
+  inject : thm list list,
+  exhaustion : thm list,
+  rec_thms : thm list,
+  case_thms : thm list list,
+  split_thms : (thm * thm) list,
+  induction : thm,
+  simps : thm list}
+
+structure DatatypeInterpretation = InterpretationFun
+  (type T = datatype_config * string list val eq = eq_snd op =);
+fun interpretation f = DatatypeInterpretation.interpretation (uncurry f);
 
 
 (******************* definitional introduction of datatypes *******************)
 
-fun add_datatype_def flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
+fun add_datatype_def (config : datatype_config) new_type_names descr sorts types_syntax constr_syntax dt_info
     case_names_induct case_names_exhausts thy =
   let
-    val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names);
+    val _ = message config ("Proofs for datatype(s) " ^ commas_quote new_type_names);
 
     val ((inject, distinct, dist_rewrites, simproc_dists, induct), thy2) = thy |>
-      DatatypeRepProofs.representation_proofs flat_names dt_info new_type_names descr sorts
+      DatatypeRepProofs.representation_proofs config dt_info new_type_names descr sorts
         types_syntax constr_syntax case_names_induct;
 
-    val (casedist_thms, thy3) = DatatypeAbsProofs.prove_casedist_thms new_type_names descr
+    val (casedist_thms, thy3) = DatatypeAbsProofs.prove_casedist_thms config new_type_names descr
       sorts induct case_names_exhausts thy2;
     val ((reccomb_names, rec_thms), thy4) = DatatypeAbsProofs.prove_primrec_thms
-      flat_names new_type_names descr sorts dt_info inject dist_rewrites
+      config new_type_names descr sorts dt_info inject dist_rewrites
       (Simplifier.theory_context thy3 dist_ss) induct thy3;
     val ((case_thms, case_names), thy6) = DatatypeAbsProofs.prove_case_thms
-      flat_names new_type_names descr sorts reccomb_names rec_thms thy4;
-    val (split_thms, thy7) = DatatypeAbsProofs.prove_split_thms new_type_names
+      config new_type_names descr sorts reccomb_names rec_thms thy4;
+    val (split_thms, thy7) = DatatypeAbsProofs.prove_split_thms config new_type_names
       descr sorts inject dist_rewrites casedist_thms case_thms thy6;
-    val (nchotomys, thy8) = DatatypeAbsProofs.prove_nchotomys new_type_names
+    val (nchotomys, thy8) = DatatypeAbsProofs.prove_nchotomys config new_type_names
       descr sorts casedist_thms thy7;
     val (case_congs, thy9) = DatatypeAbsProofs.prove_case_congs new_type_names
       descr sorts nchotomys case_thms thy8;
@@ -406,7 +399,7 @@
       |> add_cases_induct dt_infos induct
       |> Sign.parent_path
       |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
-      |> DatatypeInterpretation.data (map fst dt_infos);
+      |> DatatypeInterpretation.data (config, map fst dt_infos);
   in
     ({distinct = distinct,
       inject = inject,
@@ -421,7 +414,7 @@
 
 (*********************** declare existing type as datatype *********************)
 
-fun prove_rep_datatype alt_names new_type_names descr sorts induct inject half_distinct thy =
+fun prove_rep_datatype (config : datatype_config) alt_names new_type_names descr sorts induct inject half_distinct thy =
   let
     val ((_, [induct']), _) =
       Variable.importT_thms [induct] (Variable.thm_context induct);
@@ -440,19 +433,19 @@
     val (case_names_induct, case_names_exhausts) =
       (mk_case_names_induct descr, mk_case_names_exhausts descr (map #1 dtnames));
 
-    val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names);
+    val _ = message config ("Proofs for datatype(s) " ^ commas_quote new_type_names);
 
     val (casedist_thms, thy2) = thy |>
-      DatatypeAbsProofs.prove_casedist_thms new_type_names [descr] sorts induct
+      DatatypeAbsProofs.prove_casedist_thms config new_type_names [descr] sorts induct
         case_names_exhausts;
     val ((reccomb_names, rec_thms), thy3) = DatatypeAbsProofs.prove_primrec_thms
-      false new_type_names [descr] sorts dt_info inject distinct
+      config new_type_names [descr] sorts dt_info inject distinct
       (Simplifier.theory_context thy2 dist_ss) induct thy2;
-    val ((case_thms, case_names), thy4) = DatatypeAbsProofs.prove_case_thms false
-      new_type_names [descr] sorts reccomb_names rec_thms thy3;
+    val ((case_thms, case_names), thy4) = DatatypeAbsProofs.prove_case_thms
+      config new_type_names [descr] sorts reccomb_names rec_thms thy3;
     val (split_thms, thy5) = DatatypeAbsProofs.prove_split_thms
-      new_type_names [descr] sorts inject distinct casedist_thms case_thms thy4;
-    val (nchotomys, thy6) = DatatypeAbsProofs.prove_nchotomys new_type_names
+      config new_type_names [descr] sorts inject distinct casedist_thms case_thms thy4;
+    val (nchotomys, thy6) = DatatypeAbsProofs.prove_nchotomys config new_type_names
       [descr] sorts casedist_thms thy5;
     val (case_congs, thy7) = DatatypeAbsProofs.prove_case_congs new_type_names
       [descr] sorts nchotomys case_thms thy6;
@@ -482,7 +475,7 @@
       |> Sign.parent_path
       |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
       |> snd
-      |> DatatypeInterpretation.data (map fst dt_infos);
+      |> DatatypeInterpretation.data (config, map fst dt_infos);
   in
     ({distinct = distinct,
       inject = inject,
@@ -494,7 +487,7 @@
       simps = simps}, thy11)
   end;
 
-fun gen_rep_datatype prep_term after_qed alt_names raw_ts thy =
+fun gen_rep_datatype prep_term (config : datatype_config) after_qed alt_names raw_ts thy =
   let
     fun constr_of_term (Const (c, T)) = (c, T)
       | constr_of_term t =
@@ -550,7 +543,7 @@
             (*FIXME somehow dubious*)
       in
         ProofContext.theory_result
-          (prove_rep_datatype alt_names new_type_names descr vs induct injs half_distincts)
+          (prove_rep_datatype config alt_names new_type_names descr vs induct injs half_distincts)
         #-> after_qed
       end;
   in
@@ -560,13 +553,13 @@
   end;
 
 val rep_datatype = gen_rep_datatype Sign.cert_term;
-val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global (K I);
+val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global default_datatype_config (K I);
 
 
 
 (******************************** add datatype ********************************)
 
-fun gen_add_datatype prep_typ err flat_names new_type_names dts thy =
+fun gen_add_datatype prep_typ (config : datatype_config) new_type_names dts thy =
   let
     val _ = Theory.requires thy "Datatype" "datatype definitions";
 
@@ -598,7 +591,7 @@
             val _ = (case fold (curry OldTerm.add_typ_tfree_names) cargs' [] \\ tvs of
                 [] => ()
               | vs => error ("Extra type variables on rhs: " ^ commas vs))
-          in (constrs @ [((if flat_names then Sign.full_name tmp_thy else
+          in (constrs @ [((if #flat_names config then Sign.full_name tmp_thy else
                 Sign.full_name_path tmp_thy tname')
                   (Binding.map_name (Syntax.const_name mx') cname),
                    map (dtyp_of_typ new_dts) cargs')],
@@ -626,7 +619,7 @@
     val dt_info = get_datatypes thy;
     val (descr, _) = unfold_datatypes tmp_thy dts' sorts dt_info dts' i;
     val _ = check_nonempty descr handle (exn as Datatype_Empty s) =>
-      if err then error ("Nonemptiness check failed for datatype " ^ s)
+      if #strict config then error ("Nonemptiness check failed for datatype " ^ s)
       else raise exn;
 
     val descr' = flat descr;
@@ -634,12 +627,12 @@
     val case_names_exhausts = mk_case_names_exhausts descr' (map #1 new_dts);
   in
     add_datatype_def
-      flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
+      (config : datatype_config) new_type_names descr sorts types_syntax constr_syntax dt_info
       case_names_induct case_names_exhausts thy
   end;
 
 val add_datatype = gen_add_datatype cert_typ;
-val add_datatype_cmd = gen_add_datatype read_typ true;
+val add_datatype_cmd = gen_add_datatype read_typ default_datatype_config;
 
 
 
@@ -668,7 +661,7 @@
       (fn ((((NONE, _), t), _), _) => Binding.name_of t | ((((SOME t, _), _), _), _) => t) args;
     val specs = map (fn ((((_, vs), t), mx), cons) =>
       (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
-  in snd o add_datatype_cmd false names specs end;
+  in snd o add_datatype_cmd names specs end;
 
 val _ =
   OuterSyntax.command "datatype" "define inductive datatypes" K.thy_decl
diff -r cc969090c204 -r a616e56a5ec8 src/HOL/Tools/datatype_package/datatype_realizer.ML
--- a/src/HOL/Tools/datatype_package/datatype_realizer.ML	Tue Jun 16 16:36:56 2009 +0200
+++ b/src/HOL/Tools/datatype_package/datatype_realizer.ML	Tue Jun 16 16:37:07 2009 +0200
@@ -7,7 +7,7 @@
 
 signature DATATYPE_REALIZER =
 sig
-  val add_dt_realizers: string list -> theory -> theory
+  val add_dt_realizers: DatatypeAux.datatype_config -> string list -> theory -> theory
   val setup: theory -> theory
 end;
 
@@ -213,10 +213,10 @@
      (exh_name, ([], Extraction.nullt, prf_of exhaustion))] thy'
   end;
 
-fun add_dt_realizers names thy =
+fun add_dt_realizers config names thy =
   if ! Proofterm.proofs < 2 then thy
   else let
-    val _ = message "Adding realizers for induction and case analysis ..."
+    val _ = message config "Adding realizers for induction and case analysis ..."
     val infos = map (DatatypePackage.the_datatype thy) names;
     val info :: _ = infos;
   in
diff -r cc969090c204 -r a616e56a5ec8 src/HOL/Tools/datatype_package/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_package/datatype_rep_proofs.ML	Tue Jun 16 16:36:56 2009 +0200
+++ b/src/HOL/Tools/datatype_package/datatype_rep_proofs.ML	Tue Jun 16 16:37:07 2009 +0200
@@ -11,10 +11,13 @@
 
 signature DATATYPE_REP_PROOFS =
 sig
+  type datatype_config = DatatypeAux.datatype_config
+  type descr = DatatypeAux.descr
+  type datatype_info = DatatypeAux.datatype_info
   val distinctness_limit : int Config.T
   val distinctness_limit_setup : theory -> theory
-  val representation_proofs : bool -> DatatypeAux.datatype_info Symtab.table ->
-    string list -> DatatypeAux.descr list -> (string * sort) list ->
+  val representation_proofs : datatype_config -> datatype_info Symtab.table ->
+    string list -> descr list -> (string * sort) list ->
       (binding * mixfix) list -> (binding * mixfix) list list -> attribute
         -> theory -> (thm list list * thm list list * thm list list *
           DatatypeAux.simproc_dist list * thm) * theory
@@ -45,7 +48,7 @@
 
 (******************************************************************************)
 
-fun representation_proofs flat_names (dt_info : datatype_info Symtab.table)
+fun representation_proofs (config : datatype_config) (dt_info : datatype_info Symtab.table)
       new_type_names descr sorts types_syntax constr_syntax case_names_induct thy =
   let
     val Datatype_thy = ThyInfo.the_theory "Datatype" thy;
@@ -69,7 +72,7 @@
     val descr' = flat descr;
 
     val big_name = space_implode "_" new_type_names;
-    val thy1 = add_path flat_names big_name thy;
+    val thy1 = add_path (#flat_names config) big_name thy;
     val big_rec_name = big_name ^ "_rep_set";
     val rep_set_names' =
       (if length descr' = 1 then [big_rec_name] else
@@ -147,7 +150,7 @@
 
     (************** generate introduction rules for representing set **********)
 
-    val _ = message "Constructing representing sets ...";
+    val _ = message config "Constructing representing sets ...";
 
     (* make introduction rule for a single constructor *)
 
@@ -181,7 +184,7 @@
 
     val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
         InductivePackage.add_inductive_global (serial_string ())
-          {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
+          {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
            alt_name = Binding.name big_rec_name, coind = false, no_elim = true, no_ind = false,
            skip_mono = true, fork_mono = false}
           (map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') []
@@ -190,7 +193,7 @@
     (********************************* typedef ********************************)
 
     val (typedefs, thy3) = thy2 |>
-      parent_path flat_names |>
+      parent_path (#flat_names config) |>
       fold_map (fn ((((name, mx), tvs), c), name') =>
           TypedefPackage.add_typedef false (SOME (Binding.name name')) (name, tvs, mx)
             (Collect $ Const (c, UnivT')) NONE
@@ -199,7 +202,7 @@
               (resolve_tac rep_intrs 1)))
                 (types_syntax ~~ tyvars ~~
                   (Library.take (length newTs, rep_set_names)) ~~ new_type_names) ||>
-      add_path flat_names big_name;
+      add_path (#flat_names config) big_name;
 
     (*********************** definition of constructors ***********************)
 
@@ -257,19 +260,19 @@
         val cong' = standard (cterm_instantiate [(cterm_of thy cong_f, rep_const)] arg_cong);
         val dist = standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
         val (thy', defs', eqns', _) = Library.foldl ((make_constr_def tname T) (length constrs))
-          ((add_path flat_names tname thy, defs, [], 1), constrs ~~ constr_syntax)
+          ((add_path (#flat_names config) tname thy, defs, [], 1), constrs ~~ constr_syntax)
       in
-        (parent_path flat_names thy', defs', eqns @ [eqns'],
+        (parent_path (#flat_names config) thy', defs', eqns @ [eqns'],
           rep_congs @ [cong'], dist_lemmas @ [dist])
       end;
 
     val (thy4, constr_defs, constr_rep_eqns, rep_congs, dist_lemmas) = Library.foldl dt_constr_defs
-      ((thy3 |> Sign.add_consts_i iso_decls |> parent_path flat_names, [], [], [], []),
+      ((thy3 |> Sign.add_consts_i iso_decls |> parent_path (#flat_names config), [], [], [], []),
         hd descr ~~ new_type_names ~~ newTs ~~ constr_syntax);
 
     (*********** isomorphisms for new types (introduced by typedef) ***********)
 
-    val _ = message "Proving isomorphism properties ...";
+    val _ = message config "Proving isomorphism properties ...";
 
     val newT_iso_axms = map (fn (_, td) =>
       (collect_simp (#Abs_inverse td), #Rep_inverse td,
@@ -358,7 +361,7 @@
       in (thy', char_thms' @ char_thms) end;
 
     val (thy5, iso_char_thms) = apfst Theory.checkpoint (List.foldr make_iso_defs
-      (add_path flat_names big_name thy4, []) (tl descr));
+      (add_path (#flat_names config) big_name thy4, []) (tl descr));
 
     (* prove isomorphism properties *)
 
@@ -496,7 +499,7 @@
 
     (******************* freeness theorems for constructors *******************)
 
-    val _ = message "Proving freeness of constructors ...";
+    val _ = message config "Proving freeness of constructors ...";
 
     (* prove theorem  Rep_i (Constr_j ...) = Inj_j ...  *)
     
@@ -568,13 +571,13 @@
 
     val ((constr_inject', distinct_thms'), thy6) =
       thy5
-      |> parent_path flat_names
+      |> parent_path (#flat_names config)
       |> store_thmss "inject" new_type_names constr_inject
       ||>> store_thmss "distinct" new_type_names distinct_thms;
 
     (*************************** induction theorem ****************************)
 
-    val _ = message "Proving induction rule for datatypes ...";
+    val _ = message config "Proving induction rule for datatypes ...";
 
     val Rep_inverse_thms = (map (fn (_, iso, _) => iso RS subst) newT_iso_axms) @
       (map (fn r => r RS myinv_f_f RS subst) iso_inj_thms_unfolded);
diff -r cc969090c204 -r a616e56a5ec8 src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Jun 16 16:36:56 2009 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Jun 16 16:37:07 2009 +0200
@@ -191,9 +191,7 @@
                            |> safe_mk_meta_eq)))
                        thy
 
-val case_cong = fold add_case_cong
-
-val setup_case_cong = DatatypePackage.interpretation case_cong
+val setup_case_cong = DatatypePackage.interpretation (K (fold add_case_cong))
 
 
 (* setup *)
diff -r cc969090c204 -r a616e56a5ec8 src/HOL/Tools/function_package/size.ML
--- a/src/HOL/Tools/function_package/size.ML	Tue Jun 16 16:36:56 2009 +0200
+++ b/src/HOL/Tools/function_package/size.ML	Tue Jun 16 16:37:07 2009 +0200
@@ -218,7 +218,7 @@
       (new_type_names ~~ size_names)) thy''
   end;
 
-fun add_size_thms (new_type_names as name :: _) thy =
+fun add_size_thms config (new_type_names as name :: _) thy =
   let
     val info as {descr, alt_names, ...} = DatatypePackage.the_datatype thy name;
     val prefix = Long_Name.map_base_name (K (space_implode "_"
diff -r cc969090c204 -r a616e56a5ec8 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Tue Jun 16 16:36:56 2009 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Tue Jun 16 16:37:07 2009 +0200
@@ -307,8 +307,8 @@
 
     val ((dummies, dt_info), thy2) =
       thy1
-      |> add_dummies
-           (DatatypePackage.add_datatype false false (map (Binding.name_of o #2) dts))
+      |> add_dummies (DatatypePackage.add_datatype
+           { strict = false, flat_names = false, quiet = false } (map (Binding.name_of o #2) dts))
            (map (pair false) dts) []
       ||> Extraction.add_typeof_eqns_i ty_eqs
       ||> Extraction.add_realizes_eqns_i rlz_eqs;
diff -r cc969090c204 -r a616e56a5ec8 src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Tue Jun 16 16:36:56 2009 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML	Tue Jun 16 16:37:07 2009 +0200
@@ -15,7 +15,7 @@
   val mk_random_aux_eqs: theory -> DatatypeAux.descr -> (string * sort) list
     -> string list -> string list * string list -> typ list * typ list
     -> string * (term list * (term * term) list)
-  val ensure_random_datatype: string list -> theory -> theory
+  val ensure_random_datatype: DatatypeAux.datatype_config -> string list -> theory -> theory
   val eval_ref: (unit -> int -> seed -> term list option * seed) option ref
   val setup: theory -> theory
 end;
@@ -320,9 +320,9 @@
     val prefix = space_implode "_" (random_auxN :: names);
   in (prefix, (random_auxs, auxs_lhss ~~ auxs_rhss)) end;
 
-fun mk_random_datatype descr vs tycos (names, auxnames) (Ts, Us) thy =
+fun mk_random_datatype config descr vs tycos (names, auxnames) (Ts, Us) thy =
   let
-    val _ = DatatypeAux.message "Creating quickcheck generators ...";
+    val _ = DatatypeAux.message config "Creating quickcheck generators ...";
     val i = @{term "i\<Colon>code_numeral"};
     val mk_prop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq;
     fun mk_size_arg k = case DatatypeCodegen.find_shortest_path descr k
@@ -356,7 +356,7 @@
   in SOME (fn (v, _) => (v, (the o Vartab.lookup vtab) (v, 0)))
   end handle CLASS_ERROR => NONE;
 
-fun ensure_random_datatype raw_tycos thy =
+fun ensure_random_datatype config raw_tycos thy =
   let
     val pp = Syntax.pp_global thy;
     val algebra = Sign.classes_of thy;
@@ -370,7 +370,7 @@
       can (Sorts.mg_domain algebra tyco) @{sort random}) tycos;
   in if has_inst then thy
     else case perhaps_constrain thy (random_insts @ term_of_insts) raw_vs
-     of SOME constrain => mk_random_datatype descr
+     of SOME constrain => mk_random_datatype config descr
           (map constrain raw_vs) tycos (names, auxnames)
             ((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
       | NONE => thy