22     "val " ^ pat' ^ " = " ^ rhs

    22     "val " ^ pat' ^ " = " ^ rhs

    23   end;

    23   end;

    24 

    24 

    25 fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end";

    25 fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end";

    26 fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option";

    26 fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option";

    28 

    27 

    29 fun output_ml_open ml src ctxt ((txt,ovars),pos) =

    28 fun output_ml_open ml src ctxt ((txt,ovars),pos) =

    30   (ML_Context.eval_in (SOME ctxt) false pos (ml ovars txt);

    29   (ML_Context.eval_in (SOME ctxt) false pos (ml ovars txt);

    31   ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt (space_explode "\n" txt))

    30   ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt (space_explode "\n" txt))

    32 

    31