917   finally does nothing. For this you can write:

   917   finally does nothing. For this you can write:

   918 *}

   918 *}

   919 

   919 

   920 ML{*let

   920 ML{*let

   921   fun trace_top_lvl str = 

   921   fun trace_top_lvl str = 

   923 

   923 

   924   val trace_prop = OuterParse.prop >> trace_top_lvl

   924   val trace_prop = OuterParse.prop >> trace_top_lvl

   925 

   925 

   926   val kind = OuterKeyword.thy_decl

   926   val kind = OuterKeyword.thy_decl

   927 in

   927 in

   929 end *}

   929 end *}

   930 

   931 

   931 text {*

   932 text {*

   932   Now you can type

   933   Now you can type

   933 

   934 

   934   \begin{isabelle}

   935   \begin{isabelle}