src/Pure/Thy/thy_output.ML
changeset 30394 c11a1e65a2ed
parent 30390 ad591ee76c78
child 30398 d7ac4b7aa590
     1.1 --- a/src/Pure/Thy/thy_output.ML	Mon Mar 09 20:29:45 2009 +0100
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Mon Mar 09 20:34:11 2009 +0100
     1.3 @@ -590,8 +590,9 @@
     1.4  
     1.5  val _ = ml_text "ML" (fn txt => "fn _ => (" ^ txt ^ ");");
     1.6  val _ = ml_text "ML_type" (fn txt => "val _ = NONE : (" ^ txt ^ ") option;");
     1.7 -val _ = ml_text "ML_struct"
     1.8 -  (fn txt => "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;");
     1.9 +val _ = ml_text "ML_struct" (fn txt => "functor XXX() = struct structure XX = " ^ txt ^ " end;");
    1.10 +val _ = ml_text "ML_functor" (K "");  (*no check!*)
    1.11 +val _ = ml_text "ML_text" (K "");
    1.12  
    1.13  end;
    1.14