--- a/src/Pure/Thy/thy_output.ML Sun Mar 02 18:41:41 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML Sun Mar 02 19:00:45 2014 +0100
@@ -661,7 +661,7 @@
(ml_text (Binding.name "ML") (ml_enclose "fn _ => (" ");") #>
ml_text (Binding.name "ML_op") (ml_enclose "fn _ => (op " ");") #>
ml_text (Binding.name "ML_type") (ml_enclose "val _ = NONE : (" ") option;") #>
- ml_text (Binding.name "ML_struct")
+ ml_text (Binding.name "ML_structure")
(ml_enclose "functor XXX() = struct structure XX = " " end;") #>
ml_text (Binding.name "ML_functor") (* FIXME formal treatment of functor name (!?) *)