4   "output_tutorial.ML"

     4   "output_tutorial.ML"

     5   "chunks.ML"

     5   "chunks.ML"

     6   "antiquote_setup.ML"

     6   "antiquote_setup.ML"

     7 begin

     7 begin

     8 

     8 

     9 (* to have a special tag for text enclosed in ML *)

    10 (* to have a special tag for text enclosed in ML *)

    10 

    11 

    11 ML {*

    12 ML {*

    12 

    13 

    13 fun propagate_env (context as Context.Proof lthy) =

    14 fun propagate_env (context as Context.Proof lthy) =