916   finally does nothing. For this you can write:

   916   finally does nothing. For this you can write:

   917 *}

   917 *}

   918 

   918 

   919 ML{*let

   919 ML{*let

   920   fun trace_top_lvl str = 

   920   fun trace_top_lvl str = 

   922 

   922 

   923   val trace_prop = OuterParse.prop >> trace_top_lvl

   923   val trace_prop = OuterParse.prop >> trace_top_lvl

   924 

   924 

   925   val kind = OuterKeyword.thy_decl

   925   val kind = OuterKeyword.thy_decl

   926 in

   926 in

   928 end *}

   928 end *}

   929 

   930 

   930 text {*

   931 text {*

   931   Now you can type

   932   Now you can type

   932 

   933 

   933   \begin{isabelle}

   934   \begin{isabelle}