diff -r aa6f42252bf6 -r c11a1e65a2ed src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Mon Mar 09 20:29:45 2009 +0100
+++ b/src/Pure/Thy/thy_output.ML	Mon Mar 09 20:34:11 2009 +0100
@@ -590,8 +590,9 @@
 
 val _ = ml_text "ML" (fn txt => "fn _ => (" ^ txt ^ ");");
 val _ = ml_text "ML_type" (fn txt => "val _ = NONE : (" ^ txt ^ ") option;");
-val _ = ml_text "ML_struct"
-  (fn txt => "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;");
+val _ = ml_text "ML_struct" (fn txt => "functor XXX() = struct structure XX = " ^ txt ^ " end;");
+val _ = ml_text "ML_functor" (K "");  (*no check!*)
+val _ = ml_text "ML_text" (K "");
 
 end;