src/HOL/Tools/Nitpick/nitpick_util.ML
changeset 55080 b7c41accbff2
parent 54816 10d48c2a3e32
child 55889 6bfbec3dff62
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Mon Jan 20 19:05:25 2014 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Mon Jan 20 19:51:56 2014 +0100
     1.3 @@ -60,6 +60,7 @@
     1.4    val nat_T : typ
     1.5    val int_T : typ
     1.6    val simple_string_of_typ : typ -> string
     1.7 +  val num_binder_types : typ -> int
     1.8    val is_real_constr : theory -> string * typ -> bool
     1.9    val typ_of_dtyp : Datatype.descr -> (Datatype.dtyp * typ) list -> Datatype.dtyp -> typ
    1.10    val varify_type : Proof.context -> typ -> typ
    1.11 @@ -253,10 +254,12 @@
    1.12  val nat_T = @{typ nat}
    1.13  val int_T = @{typ int}
    1.14  
    1.15 -fun simple_string_of_typ (Type (s, _))     = s
    1.16 -  | simple_string_of_typ (TFree (s, _))    = s
    1.17 +fun simple_string_of_typ (Type (s, _)) = s
    1.18 +  | simple_string_of_typ (TFree (s, _)) = s
    1.19    | simple_string_of_typ (TVar ((s, _), _)) = s
    1.20  
    1.21 +val num_binder_types = BNF_Util.num_binder_types
    1.22 +
    1.23  fun is_real_constr thy (s, T) =
    1.24    case body_type T of
    1.25      Type (s', _) =>