1.1 --- a/src/HOL/Library/Refute.thy	Thu Nov 21 21:33:34 2013 +0100
     1.2 +++ b/src/HOL/Library/Refute.thy	Thu Nov 21 21:33:34 2013 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  header {* Refute *}
     1.5  
     1.6  theory Refute
     1.7 -imports Hilbert_Choice List Sledgehammer
     1.8 +imports Main
     1.9  keywords "refute" :: diag and "refute_params" :: thy_decl
    1.10  begin
    1.11  

     2.1 --- a/src/HOL/Library/refute.ML	Thu Nov 21 21:33:34 2013 +0100
     2.2 +++ b/src/HOL/Library/refute.ML	Thu Nov 21 21:33:34 2013 +0100
     2.3 @@ -392,7 +392,7 @@
     2.4  (* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL       *)
     2.5  (* ------------------------------------------------------------------------- *)
     2.6  
     2.7 -val typ_of_dtyp = ATP_Util.typ_of_dtyp
     2.8 +val typ_of_dtyp = Nitpick_Util.typ_of_dtyp
     2.9  
    2.10  (* ------------------------------------------------------------------------- *)
    2.11  (* close_form: universal closure over schematic variables in 't'             *)