diff -r f2d4dae2a10b -r 621ebd8b13c4 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Thu Aug 19 18:24:36 2010 +0800
+++ b/Nominal/NewParser.thy	Sat Aug 21 16:20:10 2010 +0800
@@ -20,48 +20,7 @@
 
 *}
 
-
-ML {* 
-(* nominal datatype parser *)
-local
-  structure P = Parse;
-  structure S = Scan
-
-  fun triple1 ((x, y), z) = (x, y, z)
-  fun triple2 (x, (y, z)) = (x, y, z)
-  fun tuple ((x, y, z), u) = (x, y, z, u)
-  fun tswap (((x, y), z), u) = (x, y, u, z)
-in
-
-val _ = Keyword.keyword "bind"
-val _ = Keyword.keyword "bind_set"
-val _ = Keyword.keyword "bind_res"
-
-val anno_typ = S.option (P.name --| P.$$$ "::") -- P.typ
-
-val bind_mode = P.$$$ "bind" || P.$$$ "bind_set" || P.$$$ "bind_res"
-
-val bind_clauses = 
-  P.enum "," (bind_mode -- S.repeat1 P.term -- (P.$$$ "in" |-- S.repeat1 P.name) >> triple1)
-
-val cnstr_parser =
-  P.binding -- S.repeat anno_typ -- bind_clauses -- P.opt_mixfix >> tswap
-
-(* datatype parser *)
-val dt_parser =
-  (P.type_args -- P.binding -- P.opt_mixfix >> triple1) -- 
-    (P.$$$ "=" |-- P.enum1 "|" cnstr_parser) >> tuple
-
-(* binding function parser *)
-val bnfun_parser = 
-  S.optional (P.$$$ "binder" |-- P.fixes -- Parse_Spec.where_alt_specs) ([], [])
-
-(* main parser *)
-val main_parser =
-  P.and_list1 dt_parser -- bnfun_parser >> triple2
-
-end
-*}
+ML {* print_depth 50 *}
 
 ML {*
 fun get_cnstrs dts =
@@ -744,16 +703,12 @@
  
   fun prep_body env bn_str = index_lookup env bn_str
 
-  fun prep_mode "bind"     = Lst 
-    | prep_mode "bind_set" = Set 
-    | prep_mode "bind_res" = Res 
-
   fun prep_bclause env (mode, binders, bodies) = 
   let
     val binders' = map (prep_binder env) binders
     val bodies' = map (prep_body env) bodies
   in  
-    BC (prep_mode mode, binders', bodies')
+    BC (mode, binders', bodies')
   end
 
   fun prep_bclauses (annos, bclause_strs) = 
@@ -812,7 +767,51 @@
 in
   timeit (fn () => nominal_datatype2 dts bn_funs bn_eqs bclauses' lthy |> snd)
 end
+*}
 
+ML {* 
+(* nominal datatype parser *)
+local
+  structure P = Parse;
+  structure S = Scan
+
+  fun triple1 ((x, y), z) = (x, y, z)
+  fun triple2 (x, (y, z)) = (x, y, z)
+  fun tuple ((x, y, z), u) = (x, y, z, u)
+  fun tswap (((x, y), z), u) = (x, y, u, z)
+in
+
+val _ = Keyword.keyword "bind"
+val _ = Keyword.keyword "set"
+val _ = Keyword.keyword "res"
+val _ = Keyword.keyword "list"
+
+val anno_typ = S.option (P.name --| P.$$$ "::") -- P.typ
+
+val bind_mode = P.$$$ "bind" |--
+  S.optional (Args.parens 
+    (P.$$$ "list" >> K Lst || P.$$$ "set" >> K Set || P.$$$ "res" >> K Res)) Lst
+
+val bind_clauses = 
+  P.enum "," (bind_mode -- S.repeat1 P.term -- (P.$$$ "in" |-- S.repeat1 P.name) >> triple1)
+
+val cnstr_parser =
+  P.binding -- S.repeat anno_typ -- bind_clauses -- P.opt_mixfix >> tswap
+
+(* datatype parser *)
+val dt_parser =
+  (P.type_args -- P.binding -- P.opt_mixfix >> triple1) -- 
+    (P.$$$ "=" |-- P.enum1 "|" cnstr_parser) >> tuple
+
+(* binding function parser *)
+val bnfun_parser = 
+  S.optional (P.$$$ "binder" |-- P.fixes -- Parse_Spec.where_alt_specs) ([], [])
+
+(* main parser *)
+val main_parser =
+  P.and_list1 dt_parser -- bnfun_parser >> triple2
+
+end
 
 (* Command Keyword *)