changeset 311 | ee864694315b |
parent 302 | 0cbd34857b9e |
child 315 | de49d5780f57 |
--- 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