1.1 --- a/src/HOL/Codatatype/Tools/bnf_util.ML	Mon Sep 17 15:38:16 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_util.ML	Mon Sep 17 16:57:22 2012 +0200
     1.3 @@ -58,6 +58,7 @@
     1.4      (term list * (string * typ) list) * Proof.context
     1.5    val mk_Freess': string -> typ list list -> Proof.context ->
     1.6      (term list list * (string * typ) list list) * Proof.context
     1.7 +  val nonzero_string_of_int: int -> string
     1.8  
     1.9    val strip_typeN: int -> typ -> typ list * typ
    1.10  
    1.11 @@ -286,6 +287,9 @@
    1.12  
    1.13  (** Fresh variables **)
    1.14  
    1.15 +fun nonzero_string_of_int 0 = ""
    1.16 +  | nonzero_string_of_int n = string_of_int n;
    1.17 +
    1.18  val mk_TFrees' = apfst (map TFree) oo Variable.invent_types;
    1.19  
    1.20  fun mk_TFrees n = mk_TFrees' (replicate n HOLogic.typeS);