src/Pure/Thy/thy_output.ML
changeset 36163 823c9400eb62
parent 35399 3881972fcfca
child 36323 655e2d74de3a
     1.1 --- a/src/Pure/Thy/thy_output.ML	Fri Apr 16 10:52:10 2010 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Fri Apr 16 11:39:08 2010 +0200
     1.3 @@ -599,7 +599,7 @@
     1.4  val _ = ml_text "ML" (fn txt => "fn _ => (" ^ txt ^ ");");
     1.5  val _ = ml_text "ML_type" (fn txt => "val _ = NONE : (" ^ txt ^ ") option;");
     1.6  val _ = ml_text "ML_struct" (fn txt => "functor XXX() = struct structure XX = " ^ txt ^ " end;");
     1.7 -val _ = ml_text "ML_functor" (K "");  (*no check!*)
     1.8 +val _ = ml_text "ML_functor" (fn txt => "ML_Env.check_functor " ^ ML_Syntax.print_string txt);
     1.9  val _ = ml_text "ML_text" (K "");
    1.10  
    1.11  end;