--- a/Nominal/NewParser.thy	Thu May 27 18:40:10 2010 +0200
+++ b/Nominal/NewParser.thy	Mon May 31 19:57:29 2010 +0200
@@ -140,7 +140,7 @@
 fun rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs =
 let
   val bn_funs' = map (fn (bn, ty, mx) => 
-    (raw_bind bn, replace_typ dts_env ty, mx)) bn_funs
+    (raw_bind bn, SOME (replace_typ dts_env ty), mx)) bn_funs
   
   val bn_eqs' = map (fn (attr, trm) => 
     (attr, replace_term (cnstrs_env @ bn_fun_env) dts_env trm)) bn_eqs
@@ -229,6 +229,8 @@
 end
 *}
 
+ML {* rawify_bn_funs *}
+
 ML {*
 fun raw_nominal_decls dts bn_funs bn_eqs binds lthy =
 let
@@ -254,20 +256,37 @@
     (bn_fun_strs ~~ bn_fun_strs')
   
   val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env
-  val raw_dt_names' =  map (Long_Name.qualify thy_name) raw_dt_names
   val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs 
   val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env binds 
 
   val (raw_dt_full_names, lthy1) = add_datatype_wrapper raw_dt_names raw_dts lthy
-  val (raw_bn_funs', raw_bn_eqs', lthy2) = add_primrec_wrapper raw_bn_funs raw_bn_eqs lthy1
+   
+in
+  (dt_full_names', raw_dt_full_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy1)
+end
+*}
+
+ML {*
+fun raw_bn_decls dt_names dts raw_bn_funs raw_bn_eqs constr_thms lthy =
+let
+  val (_, lthy2) = Function.add_function raw_bn_funs raw_bn_eqs
+    Function_Common.default_config (pat_completeness_simp constr_thms) lthy
+
+  val (info, lthy3) = prove_termination (Local_Theory.restore lthy2)
+  val {fs, simps, inducts, ...} = info;
+
+  val raw_bn_induct = Rule_Cases.strict_mutual_rule lthy3 (the inducts)
+  val raw_bn_eqs = the simps
 
   val raw_bn_info = 
-    prep_bn_info lthy dt_full_names' raw_dts (map prop_of raw_bn_eqs')
+    prep_bn_info lthy dt_names dts (map prop_of raw_bn_eqs)
+
 in
-  (raw_dt_full_names, raw_bclauses, raw_bn_funs', raw_bn_eqs', raw_bn_info, lthy2)
+  (fs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3)
 end
 *}
 
+
 lemma equivp_hack: "equivp x"
 sorry
 ML {*
@@ -368,24 +387,31 @@
 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy =
 let
   (* definition of the raw datatypes *)
-  val (raw_dt_names, raw_bclauses, raw_bn_funs, raw_bn_eqs, raw_bn_info, lthy1) =
+  val (dt_names, raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy0) =
     if get_STEPS lthy > 1 
     then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy
     else raise TEST lthy
 
-  val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names)
+  val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names)
   val {descr, sorts, ...} = dtinfo
   val all_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr
   val all_full_tnames = map (fn (_, (n, _, _)) => n) descr
-  val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy1)) all_full_tnames
+  val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) all_full_tnames
   
   val inject_thms = flat (map #inject dtinfos);
   val distinct_thms = flat (map #distinct dtinfos);
+  val constr_thms = inject_thms @ distinct_thms
   val rel_dtinfos = List.take (dtinfos, (length dts)); 
   val raw_constrs_distinct = (map #distinct rel_dtinfos); 
   val induct_thm = #induct dtinfo;
   val exhaust_thms = map #exhaust dtinfos;
 
+  val (raw_bn_funs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy1) =
+    if get_STEPS lthy0 > 1 
+    then raw_bn_decls dt_names raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy0
+    else raise TEST lthy0
+
+
   val bn_nos = map (fn (_, i, _) => i) raw_bn_info;
   val bns = raw_bn_funs ~~ bn_nos;
 
@@ -407,7 +433,7 @@
 
   val (raw_fvs, raw_fv_bns, raw_fv_defs, lthy3a) = 
     if get_STEPS lthy2 > 3 
-    then define_raw_fvs descr sorts raw_bn_info raw_bclauses lthy3
+    then define_raw_fvs descr sorts raw_bn_info raw_bclauses constr_thms lthy3
     else raise TEST lthy3
 
   (* definition of raw alphas *)