# HG changeset patch
# User blanchet
# Date 1385066014 -3600
# Node ID dd511ddcb203d00c05490a76863e2eca59c31874
# Parent  e8c5e95d338b3bdf1877c14e49fb2efd1ec46bd0
compile

diff -r e8c5e95d338b -r dd511ddcb203 src/HOL/Library/Refute.thy
--- a/src/HOL/Library/Refute.thy	Thu Nov 21 21:33:34 2013 +0100
+++ b/src/HOL/Library/Refute.thy	Thu Nov 21 21:33:34 2013 +0100
@@ -8,7 +8,7 @@
 header {* Refute *}
 
 theory Refute
-imports Hilbert_Choice List Sledgehammer
+imports Main
 keywords "refute" :: diag and "refute_params" :: thy_decl
 begin
 
diff -r e8c5e95d338b -r dd511ddcb203 src/HOL/Library/refute.ML
--- a/src/HOL/Library/refute.ML	Thu Nov 21 21:33:34 2013 +0100
+++ b/src/HOL/Library/refute.ML	Thu Nov 21 21:33:34 2013 +0100
@@ -392,7 +392,7 @@
 (* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL       *)
 (* ------------------------------------------------------------------------- *)
 
-val typ_of_dtyp = ATP_Util.typ_of_dtyp
+val typ_of_dtyp = Nitpick_Util.typ_of_dtyp
 
 (* ------------------------------------------------------------------------- *)
 (* close_form: universal closure over schematic variables in 't'             *)