src/HOL/Tools/Nitpick/nitpick_scope.ML
changeset 36380 1e8fcaccb3e8
parent 35968 b7f98ff9c7d9
child 36384 76d5fd5a45fb
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Fri Apr 23 19:16:52 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Fri Apr 23 19:18:39 2010 +0200
@@ -194,11 +194,8 @@
               else
                 [])
   in
-    if null ss then
-      []
-    else
-      Sledgehammer_Util.serial_commas "and" ss
-      |> map Pretty.str |> Pretty.breaks
+    if null ss then []
+    else serial_commas "and" ss |> map Pretty.str |> Pretty.breaks
   end
 
 (* scope -> string *)