--- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Tue Nov 19 18:34:04 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Tue Nov 19 18:38:25 2013 +0100
@@ -293,4 +293,4 @@
of_indent 0 ^ (if n <> 1 then "next" else "qed")
end
-end
+end;