equal
deleted
inserted
replaced
588 |
588 |
589 in |
589 in |
590 |
590 |
591 val _ = ml_text "ML" (fn txt => "fn _ => (" ^ txt ^ ");"); |
591 val _ = ml_text "ML" (fn txt => "fn _ => (" ^ txt ^ ");"); |
592 val _ = ml_text "ML_type" (fn txt => "val _ = NONE : (" ^ txt ^ ") option;"); |
592 val _ = ml_text "ML_type" (fn txt => "val _ = NONE : (" ^ txt ^ ") option;"); |
593 val _ = ml_text "ML_struct" |
593 val _ = ml_text "ML_struct" (fn txt => "functor XXX() = struct structure XX = " ^ txt ^ " end;"); |
594 (fn txt => "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;"); |
594 val _ = ml_text "ML_functor" (K ""); (*no check!*) |
595 |
595 val _ = ml_text "ML_text" (K ""); |
596 end; |
596 |
597 |
597 end; |
598 end; |
598 |
|
599 end; |