src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
changeset 42680 b6c27cf04fe9
parent 42290 b1f544c84040
child 42697 9bc5dc48f1a5
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed May 04 18:48:25 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed May 04 19:35:48 2011 +0200
     1.3 @@ -15,6 +15,9 @@
     1.4    val nat_subscript : int -> string
     1.5    val unyxml : string -> string
     1.6    val maybe_quote : string -> string
     1.7 +  val typ_of_dtyp :
     1.8 +    Datatype_Aux.descr -> (Datatype_Aux.dtyp * typ) list -> Datatype_Aux.dtyp
     1.9 +    -> typ
    1.10    val monomorphic_term : Type.tyenv -> term -> term
    1.11    val eta_expand : typ list -> term -> int -> term
    1.12    val transform_elim_term : term -> term
    1.13 @@ -80,6 +83,15 @@
    1.14             Keyword.is_keyword s) ? quote
    1.15    end
    1.16  
    1.17 +fun typ_of_dtyp _ typ_assoc (Datatype_Aux.DtTFree a) =
    1.18 +    the (AList.lookup (op =) typ_assoc (Datatype_Aux.DtTFree a))
    1.19 +  | typ_of_dtyp descr typ_assoc (Datatype_Aux.DtType (s, Us)) =
    1.20 +    Type (s, map (typ_of_dtyp descr typ_assoc) Us)
    1.21 +  | typ_of_dtyp descr typ_assoc (Datatype_Aux.DtRec i) =
    1.22 +    let val (s, ds, _) = the (AList.lookup (op =) descr i) in
    1.23 +      Type (s, map (typ_of_dtyp descr typ_assoc) ds)
    1.24 +    end
    1.25 +
    1.26  fun monomorphic_term subst t =
    1.27    map_types (map_type_tvar (fn v =>
    1.28        case Type.lookup subst v of