src/HOL/Tools/datatype_aux.ML
changeset 5661 6ecb6ea25f19
parent 5177 0d3a168e4d44
child 5891 92e0f5e6fd17
     1.1 --- a/src/HOL/Tools/datatype_aux.ML	Fri Oct 16 18:52:17 1998 +0200
     1.2 +++ b/src/HOL/Tools/datatype_aux.ML	Fri Oct 16 18:54:55 1998 +0200
     1.3 @@ -8,10 +8,16 @@
     1.4  
     1.5  signature DATATYPE_AUX =
     1.6  sig
     1.7 +  val quiet_mode : bool ref
     1.8 +  val message : string -> unit
     1.9 +  
    1.10    val foldl1 : ('a * 'a -> 'a) -> 'a list -> 'a
    1.11  
    1.12    val get_thy : string -> theory -> theory option
    1.13  
    1.14 +  val add_path : bool -> string -> theory -> theory
    1.15 +  val parent_path : bool -> theory -> theory
    1.16 +
    1.17    val store_thmss : string -> string list -> thm list list -> theory -> theory
    1.18    val store_thms : string -> string list -> thm list -> theory -> theory
    1.19  
    1.20 @@ -55,27 +61,33 @@
    1.21  structure DatatypeAux : DATATYPE_AUX =
    1.22  struct
    1.23  
    1.24 +val quiet_mode = ref false;
    1.25 +fun message s = if !quiet_mode then () else writeln s;
    1.26 +
    1.27  (* FIXME: move to library ? *)
    1.28  fun foldl1 f (x::xs) = foldl f (x, xs);
    1.29  
    1.30  fun get_thy name thy = find_first
    1.31    (equal name o Sign.name_of o sign_of) (ancestors_of thy);
    1.32  
    1.33 +fun add_path flat_names s = if flat_names then I else Theory.add_path s;
    1.34 +fun parent_path flat_names = if flat_names then I else Theory.parent_path;
    1.35 +
    1.36  (* store theorems in theory *)
    1.37  
    1.38  fun store_thmss label tnames thmss thy =
    1.39    foldr (fn ((tname, thms), thy') => thy' |>
    1.40 -    (if length tnames = 1 then I else Theory.add_path tname) |>
    1.41 +    Theory.add_path tname |>
    1.42      PureThy.add_tthmss [((label, map Attribute.tthm_of thms), [])] |>
    1.43 -    (if length tnames = 1 then I else Theory.parent_path))
    1.44 -    (tnames ~~ thmss, thy);
    1.45 +    Theory.parent_path)
    1.46 +      (tnames ~~ thmss, thy);
    1.47  
    1.48  fun store_thms label tnames thms thy =
    1.49    foldr (fn ((tname, thm), thy') => thy' |>
    1.50 -    (if length tnames = 1 then I else Theory.add_path tname) |>
    1.51 +    Theory.add_path tname |>
    1.52      PureThy.add_tthms [((label, Attribute.tthm_of thm), [])] |>
    1.53 -    (if length tnames = 1 then I else Theory.parent_path))
    1.54 -    (tnames ~~ thms, thy);
    1.55 +    Theory.parent_path)
    1.56 +      (tnames ~~ thms, thy);
    1.57  
    1.58  (* split theorem thm_1 & ... & thm_n into n theorems *)
    1.59