21 binder

    21 binder

    22   bn::"assg \<Rightarrow> atom list"

    22   bn::"assg \<Rightarrow> atom list"

    23 where

    23 where

    24  "bn (As x y t a) = [atom x] @ bn a"

    24  "bn (As x y t a) = [atom x] @ bn a"

    25 | "bn (As_Nil) = []"

    25 | "bn (As_Nil) = []"

    26 

    28 

    27 ML {* 

    29 ML {* 

    28   Variable.import;

    30   Variable.import;

    29   Variable.import true @{thms foo.exhaust} @{context}

    31   Variable.import true @{thms foo.exhaust} @{context}

    30 *}

    32 *}