651     ||>> prepare_bn_funs bn_fun_strs bn_eq_strs 

   651     ||>> prepare_bn_funs bn_fun_strs bn_eq_strs 

   652     ||>> prepare_bclauses dt_strs 

   652     ||>> prepare_bclauses dt_strs 

   653 

   653 

   654   val bclauses' = complete dt_strs bclauses

   654   val bclauses' = complete dt_strs bclauses

   655 in

   655 in

   657 end

   657 end

   658 *}

   658 *}

   659 

   659 

   660 ML {* 

   660 ML {* 

   661 (* nominal datatype parser *)

   661 (* nominal datatype parser *)

   703 (* Command Keyword *)

   703 (* Command Keyword *)

   704 val _ = Outer_Syntax.local_theory "nominal_datatype" "test" Keyword.thy_decl

   704 val _ = Outer_Syntax.local_theory "nominal_datatype" "test" Keyword.thy_decl

   705   (main_parser >> nominal_datatype2_cmd)

   705   (main_parser >> nominal_datatype2_cmd)

   706 *}

   706 *}

   707 

   707 

   708 ML {*

   709 ML {*

   709 trace := true

   710 trace := true

   710 *}

   711 *}