src/HOL/Tools/meson.ML

--- a/src/HOL/Tools/meson.ML	Wed Oct 11 10:49:29 2006 +0200
+++ b/src/HOL/Tools/meson.ML	Wed Oct 11 10:49:36 2006 +0200
@@ -273,8 +273,9 @@
 
 (*Remove duplicate literals, if there are any*)
 fun nodups th =
-    if null(findrep(literals(prop_of th))) then th
-    else nodups_aux [] th;
+  if has_duplicates (op =) (literals (prop_of th))
+    then nodups_aux [] th
+    else th;
 
 
 (**** Generation of contrapositives ****)