--- a/src/HOL/Library/refute.ML Mon Mar 03 22:33:22 2014 +0100
+++ b/src/HOL/Library/refute.ML Mon Mar 03 22:33:22 2014 +0100
@@ -372,7 +372,15 @@
(* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL *)
(* ------------------------------------------------------------------------- *)
-val typ_of_dtyp = Nitpick_Util.typ_of_dtyp
+fun typ_of_dtyp _ typ_assoc (Datatype.DtTFree a) =
+ the (AList.lookup (op =) typ_assoc (Datatype.DtTFree a))
+ | typ_of_dtyp descr typ_assoc (Datatype.DtType (s, Us)) =
+ Type (s, map (typ_of_dtyp descr typ_assoc) Us)
+ | typ_of_dtyp descr typ_assoc (Datatype.DtRec i) =
+ let val (s, ds, _) = the (AList.lookup (op =) descr i) in
+ Type (s, map (typ_of_dtyp descr typ_assoc) ds)
+ end
+
val close_form = ATP_Util.close_form
val monomorphic_term = ATP_Util.monomorphic_term
val specialize_type = ATP_Util.specialize_type