--- a/ProgTutorial/output_tutorial.ML	Mon Aug 03 14:01:57 2009 +0200
+++ b/ProgTutorial/output_tutorial.ML	Mon Aug 03 16:47:01 2009 +0200
@@ -3,7 +3,7 @@
 struct
 
 (* rebuilding the output function from ThyOutput in order to *)
-(* enable the options [gray, linenos, index]                   *)
+(* enable the options [gray, linenos, index]                 *)
 
 val gray = ref false
 val linenos = ref false
@@ -26,11 +26,12 @@
     #> enclose "\\isa{" "}")
 end
 
+
 datatype qstring =
   NoString
-| Plain  of string
-| Code   of string
-| IStruc of string
+| Plain   of string
+| Code    of string
+| IStruct of string
 
 datatype entry = 
    No_Entry
@@ -67,7 +68,7 @@
 fun get_qstring NoString = ""
   | get_qstring (Plain s) = get_word s
   | get_qstring (Code s) = let val w = get_word s in  (w ^ "@{\\tt\\slshape{}" ^ w ^ "}") end
-  | get_qstring (IStruc s) =  "in {\\tt\\slshape{}" ^ (get_word s) ^ "}"
+  | get_qstring (IStruct s) =  "in {\\tt\\slshape{}" ^ (get_word s) ^ "}"
 
 fun is_empty_qstr (Plain "") = true
   | is_empty_qstr (Code "") = true