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 ****)