diff -r 007922777ff1 -r ee864694315b ProgTutorial/output_tutorial.ML
--- a/ProgTutorial/output_tutorial.ML	Mon Aug 17 20:57:32 2009 +0200
+++ b/ProgTutorial/output_tutorial.ML	Tue Aug 18 01:05:56 2009 +0200
@@ -8,6 +8,7 @@
 val gray = ref false
 val linenos = ref false
 
+
 fun output txt =
 let
   val prts = map Pretty.str txt
@@ -26,7 +27,6 @@
     #> enclose "\\isa{" "}")
 end
 
-
 datatype qstring =
   NoString
 | Plain   of string