--- a/Nominal/NewParser.thy	Sun Apr 25 01:31:22 2010 +0200
+++ b/Nominal/NewParser.thy	Sun Apr 25 07:54:28 2010 +0200
@@ -41,11 +41,11 @@
 
 (* binding function parser *)
 val bnfun_parser = 
-  S.optional (P.$$$ "binder" |-- P.fixes -- SpecParse.where_alt_specs) ([],[])
+  S.optional (P.$$$ "binder" |-- P.fixes -- SpecParse.where_alt_specs) ([], [])
 
 (* main parser *)
 val main_parser =
-  (P.and_list1 dt_parser) -- bnfun_parser >> triple2
+  P.and_list1 dt_parser -- bnfun_parser >> triple2
 
 end
 *}
@@ -94,6 +94,9 @@
 end
 *}
 
+
+text {* Infrastructure for adding "_raw" to types and terms *}
+
 ML {*
 fun add_raw s = s ^ "_raw"
 fun add_raws ss = map add_raw ss
@@ -254,7 +257,6 @@
   val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env binds 
 
   val raw_bns = prep_bn dt_full_names' raw_dts (map snd raw_bn_eqs)
-
 in
   lthy 
   |> add_datatype_wrapper raw_dt_names raw_dts 
@@ -424,13 +426,10 @@
 fun nominal_datatype2_cmd (dt_strs, bn_fun_strs, bn_eq_strs) lthy = 
 let
   fun prep_typ (tvs, tname, mx, _) = (tname, length tvs, mx)
-
   val lthy0 = 
     Local_Theory.theory (Sign.add_types (map prep_typ dt_strs)) lthy
-  val (dts, lthy1) = 
-    prepare_dts dt_strs lthy0
-  val ((bn_funs, bn_eqs), lthy2) = 
-    prepare_bn_funs bn_fun_strs bn_eq_strs lthy1
+  val (dts, lthy1) = prepare_dts dt_strs lthy0
+  val ((bn_funs, bn_eqs), lthy2) = prepare_bn_funs bn_fun_strs bn_eq_strs lthy1
   val bclauses = prepare_bclauses dt_strs lthy2
   val bclauses' = complete dt_strs bclauses 
 in
@@ -495,11 +494,6 @@
 thm exp_raw_fnclause_raw_fnclauses_raw_lrb_raw_lrbs_raw_pat_raw.induct[no_vars]
 thm b_fnclause_raw_b_fnclauses_raw_b_lrb_raw_b_lrbs_raw_b_pat_raw.simps[no_vars]
 
-text {*
-  Why does it take so long to define the nominal
-  datatype? Is it the function definitions?
-  
-*}
 
 
 end