4   "~~/src/HOL/Library/Monad_Syntax"

     4   "~~/src/HOL/Library/Monad_Syntax"

     5 begin

     5 begin

     6 

     6 

     7 

     7 

     8 atom_decl name

     8 atom_decl name

     9 

    10 

    10 ML {* trace := true *}

    11 ML {* trace := true *}

    11 

    12 

    12 nominal_datatype lam =

    13 nominal_datatype lam =

    13   Var "name"

    14   Var "name"