diff -r bd7927cca152 -r d1a9b07783ab src/HOL/Library/refute.ML
--- 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