src/HOL/Tools/refute.ML
changeset 42680 b6c27cf04fe9
parent 42364 8c674b3b8e44
child 43085 0a2f5b86bdd7
     1.1 --- a/src/HOL/Tools/refute.ML	Wed May 04 18:48:25 2011 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Wed May 04 19:35:48 2011 +0200
     1.3 @@ -71,7 +71,6 @@
     1.4    val is_IDT_recursor : theory -> string * typ -> bool
     1.5    val is_const_of_class: theory -> string * typ -> bool
     1.6    val string_of_typ : typ -> string
     1.7 -  val typ_of_dtyp : Datatype.descr -> (Datatype.dtyp * typ) list -> Datatype.dtyp -> typ
     1.8  end;
     1.9  
    1.10  structure Refute : REFUTE =
    1.11 @@ -394,17 +393,7 @@
    1.12  (* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL       *)
    1.13  (* ------------------------------------------------------------------------- *)
    1.14  
    1.15 -fun typ_of_dtyp descr typ_assoc (Datatype_Aux.DtTFree a) =
    1.16 -      (* replace a 'DtTFree' variable by the associated type *)
    1.17 -      the (AList.lookup (op =) typ_assoc (Datatype_Aux.DtTFree a))
    1.18 -  | typ_of_dtyp descr typ_assoc (Datatype_Aux.DtType (s, ds)) =
    1.19 -      Type (s, map (typ_of_dtyp descr typ_assoc) ds)
    1.20 -  | typ_of_dtyp descr typ_assoc (Datatype_Aux.DtRec i) =
    1.21 -      let
    1.22 -        val (s, ds, _) = the (AList.lookup (op =) descr i)
    1.23 -      in
    1.24 -        Type (s, map (typ_of_dtyp descr typ_assoc) ds)
    1.25 -      end;
    1.26 +val typ_of_dtyp = Sledgehammer_Util.typ_of_dtyp
    1.27  
    1.28  (* ------------------------------------------------------------------------- *)
    1.29  (* close_form: universal closure over schematic variables in 't'             *)