src/HOL/Tools/meson.ML

 			   [disj_FalseD1, disj_FalseD2, asm_rl])
     handle THM _ => th;
 
 (*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 ****)
 
 (*Associate disjuctions to right -- make leftmost disjunct a LITERAL*)