src/HOL/Library/refute.ML
changeset 54556 dd511ddcb203
parent 51685 385ef6706252
child 54757 4960647932ec
     1.1 --- a/src/HOL/Library/refute.ML	Thu Nov 21 21:33:34 2013 +0100
     1.2 +++ b/src/HOL/Library/refute.ML	Thu Nov 21 21:33:34 2013 +0100
     1.3 @@ -392,7 +392,7 @@
     1.4  (* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL       *)
     1.5  (* ------------------------------------------------------------------------- *)
     1.6  
     1.7 -val typ_of_dtyp = ATP_Util.typ_of_dtyp
     1.8 +val typ_of_dtyp = Nitpick_Util.typ_of_dtyp
     1.9  
    1.10  (* ------------------------------------------------------------------------- *)
    1.11  (* close_form: universal closure over schematic variables in 't'             *)