changeset 328 | c0cae24b9d46 |
parent 316 | 74f0a06f751f |
child 351 | f118240ab44a |
--- a/ProgTutorial/output_tutorial.ML Fri Oct 02 15:38:14 2009 +0200 +++ b/ProgTutorial/output_tutorial.ML Sat Oct 03 13:01:39 2009 +0200 @@ -5,8 +5,8 @@ (* rebuilding the output function from ThyOutput in order to *) (* enable the options [gray, linenos] *) -val gray = ref false -val linenos = ref false +val gray = Unsynchronized.ref false +val linenos = Unsynchronized.ref false fun output txt =