src/HOL/Tools/meson.ML
changeset 20972 db0425645cc7
parent 20822 634070b40731
child 21046 fe1db2f991a7
     1.1 --- a/src/HOL/Tools/meson.ML	Wed Oct 11 10:49:29 2006 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Wed Oct 11 10:49:36 2006 +0200
     1.3 @@ -273,8 +273,9 @@
     1.4  
     1.5  (*Remove duplicate literals, if there are any*)
     1.6  fun nodups th =
     1.7 -    if null(findrep(literals(prop_of th))) then th
     1.8 -    else nodups_aux [] th;
     1.9 +  if has_duplicates (op =) (literals (prop_of th))
    1.10 +    then nodups_aux [] th
    1.11 +    else th;
    1.12  
    1.13  
    1.14  (**** Generation of contrapositives ****)