--- a/Nominal/Parser.thy	Mon Mar 01 19:23:08 2010 +0100
+++ b/Nominal/Parser.thy	Tue Mar 02 06:42:43 2010 +0100
@@ -144,6 +144,12 @@
 *}
 
 ML {* 
+fun rawify_binds dts_env cnstrs_env bn_fun_env binds =
+  map (map (map (map (fn (opt_trm, i, j) => 
+    (Option.map (replace_term (cnstrs_env @ bn_fun_env) dts_env) opt_trm, i, j))))) binds
+*}
+
+ML {* 
 fun add_primrec_wrapper funs eqs lthy = 
   if null funs then (([], []), lthy)
   else 
@@ -155,14 +161,20 @@
    end
 *}
 
+ML {*
+fun add_datatype_wrapper dt_names dts =
+let
+  val conf = Datatype.default_config
+in
+  Local_Theory.theory_result (Datatype.add_datatype conf dt_names dts)
+end
+*}
 
 ML {* 
-fun nominal_datatype2 dts bn_funs bn_eqs binds lthy =
+fun raw_nominal_decls dts bn_funs bn_eqs binds lthy =
 let
   val thy = ProofContext.theory_of lthy
   val thy_name = Context.theory_name thy
-  
-  val conf = Datatype.default_config
 
   val dt_names = map (fn (_, s, _, _) => Binding.name_of s) dts
   val dt_full_names = map (Long_Name.qualify thy_name) dt_names 
@@ -179,14 +191,31 @@
   val bn_fun_strs = get_bn_fun_strs bn_funs
   val bn_fun_strs' = add_raws bn_fun_strs
   val bn_fun_env = bn_fun_strs ~~ bn_fun_strs'
-
+  val bn_fun_full_env = map (pairself (Long_Name.qualify thy_name)) 
+    (bn_fun_strs ~~ bn_fun_strs')
+  
   val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env
 
   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 
 in
   lthy 
-  |> Local_Theory.theory_result (Datatype.add_datatype conf raw_dt_names raw_dts) 
+  |> add_datatype_wrapper raw_dt_names raw_dts 
   ||>> add_primrec_wrapper raw_bn_funs raw_bn_eqs
+  ||>> pair raw_binds
+end
+*}
+
+ML {* add_primrec_wrapper *}
+
+ML {* 
+fun nominal_datatype2 dts bn_funs bn_eqs binds lthy =
+let
+  val (((raw_dt_names, (raw_bn_funs, raw_bn_eqs)), raw_binds), lthy') =
+    raw_nominal_decls dts bn_funs bn_eqs binds lthy
+in
+  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy')
 end
 *}
 
@@ -312,7 +341,6 @@
     ||>> prepare_bn_funs bn_fun_strs bn_eq_strs
     ||> prepare_binds dt_strs
   
-  val _ = tracing (PolyML.makestring binds)
 in
   nominal_datatype2 dts bn_fun bn_eq binds lthy |> snd
 end