src/HOL/Tools/Datatype/datatype_aux.ML
changeset 32124 954321008785
parent 31775 2b04504fcb69
child 32712 ec5976f4d3d8
     1.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Tue Jul 21 15:44:31 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Tue Jul 21 15:52:30 2009 +0200
     1.3 @@ -22,9 +22,6 @@
     1.4  
     1.5    val message : config -> string -> unit
     1.6    
     1.7 -  val add_path : bool -> string -> theory -> theory
     1.8 -  val parent_path : bool -> theory -> theory
     1.9 -
    1.10    val store_thmss_atts : string -> string list -> attribute list list -> thm list list
    1.11      -> theory -> thm list list * theory
    1.12    val store_thmss : string -> string list -> thm list list -> theory -> thm list list * theory
    1.13 @@ -76,15 +73,12 @@
    1.14  
    1.15  (* datatype option flags *)
    1.16  
    1.17 -type config = { strict: bool, flat_names: bool, quiet: bool };
    1.18 +type config = { strict: bool, quiet: bool };
    1.19  val default_config : config =
    1.20 -  { strict = true, flat_names = false, quiet = false };
    1.21 +  { strict = true, quiet = false };
    1.22  fun message ({ quiet, ...} : config) s =
    1.23    if quiet then () else writeln s;
    1.24  
    1.25 -fun add_path flat_names s = if flat_names then I else Sign.add_path s;
    1.26 -fun parent_path flat_names = if flat_names then I else Sign.parent_path;
    1.27 -
    1.28  
    1.29  (* store theorems in theory *)
    1.30