--- a/Nominal/Parser.thy	Wed Mar 10 09:09:52 2010 +0100
+++ b/Nominal/Parser.thy	Wed Mar 10 09:10:11 2010 +0100
@@ -149,6 +149,29 @@
     (Option.map (apfst (replace_term (cnstrs_env @ bn_fun_env) dts_env)) opt_trm, i, j))))) binds
 *}
 
+ML {*
+fun prep_bn dt_names eqs lthy = 
+let
+  fun aux eq = 
+  let
+    val (lhs, rhs) = eq
+      |> strip_qnt_body "all" 
+      |> HOLogic.dest_Trueprop
+      |> HOLogic.dest_eq
+    val (head, [cnstr]) = strip_comb lhs
+    val (_, ty) = dest_Free head
+    val (ty_name, _) = dest_Type (domain_type ty)
+    val dt_index = find_index (fn x => x = ty_name) dt_names
+    val (_, cnstr_args) = strip_comb cnstr
+    val included = map (fn i => length (cnstr_args) - i - 1) (loose_bnos rhs)
+  in
+    (head, dt_index, included)
+  end  
+in
+  map aux eqs
+end
+*}
+
 ML {* 
 fun add_primrec_wrapper funs eqs lthy = 
   if null funs then (([], []), lthy)
@@ -199,11 +222,16 @@
   val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs 
   
   val raw_binds = rawify_binds dts_env cnstrs_env bn_fun_full_env binds 
+
+  val raw_bns = prep_bn dt_full_names' (map snd raw_bn_eqs) lthy
+
+  val _ = tracing (cat_lines (map PolyML.makestring raw_bns)) 
 in
   lthy 
   |> add_datatype_wrapper raw_dt_names raw_dts 
   ||>> add_primrec_wrapper raw_bn_funs raw_bn_eqs
   ||>> pair raw_binds
+  ||>> pair raw_bns
 end
 *}
 
@@ -230,7 +258,7 @@
 let
   val thy = ProofContext.theory_of lthy
   val thy_name = Context.theory_name thy
-  val (((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_binds), lthy2) =
+  val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_binds), raw_bns), lthy2) =
     raw_nominal_decls dts bn_funs bn_eqs binds lthy
   val bn_funs_decls = [];
 
@@ -392,11 +420,10 @@
 (* declaring the functions in the local theory    *)
 fun prepare_bn_funs bn_fun_strs bn_eq_strs lthy =
 let
-  fun prep_bn_fun ((bn, T), mx) = (bn, T, mx) 
-
   val ((bn_funs, bn_eqs), _) = 
     Specification.read_spec bn_fun_strs bn_eq_strs lthy
 
+  fun prep_bn_fun ((bn, T), mx) = (bn, T, mx) 
   val bn_funs' = map prep_bn_fun bn_funs
 in
   lthy
@@ -466,15 +493,15 @@
 let
   fun prep_typ (tvs, tname, mx, _) = (tname, length tvs, mx)
 
-  val ((dts, (bn_fun, bn_eq)), binds) = 
-    lthy 
-    |> Local_Theory.theory (Sign.add_types (map prep_typ dt_strs))
-    |> prepare_dts dt_strs
-    ||>> prepare_bn_funs bn_fun_strs bn_eq_strs
-    ||> prepare_binds dt_strs
-  
+  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 binds = prepare_binds dt_strs lthy2
 in
-  nominal_datatype2 dts bn_fun bn_eq binds lthy |> snd
+  nominal_datatype2 dts bn_funs bn_eqs binds lthy |> snd
 end
 *}
 

--- a/Nominal/Test.thy	Wed Mar 10 09:09:52 2010 +0100
+++ b/Nominal/Test.thy	Wed Mar 10 09:10:11 2010 +0100
@@ -66,8 +66,9 @@
   f::"pat' \<Rightarrow> atom set"
 where 
   "f PN = {}"
+| "f (PD x y) = {atom x, atom y}"
 | "f (PS x) = {atom x}"
-| "f (PD x y) = {atom x, atom y}"
+
 
 (* compat should be
 compat (PN) pi (PN) == True