--- a/Nominal/NewParser.thy	Tue May 11 18:20:25 2010 +0200
+++ b/Nominal/NewParser.thy	Wed May 12 13:43:48 2010 +0100
@@ -65,6 +65,7 @@
   map (fn (bn_fun, _, _) => Binding.name_of bn_fun) bn_funs
 *}
 
+
 ML {* 
 fun add_primrec_wrapper funs eqs lthy = 
   if null funs then (([], []), lthy)
@@ -72,8 +73,10 @@
    let 
      val eqs' = map (fn (_, eq) => (Attrib.empty_binding, eq)) eqs
      val funs' = map (fn (bn, ty, mx) => (bn, SOME ty, mx)) funs
+     val ((funs'', eqs''), lthy') = Primrec.add_primrec funs' eqs' lthy
+     val phi = ProofContext.export_morphism lthy' lthy
    in 
-     Primrec.add_primrec funs' eqs' lthy
+     ((map (Morphism.term phi) funs'', map (Morphism.thm phi) eqs''), lthy')
    end
 *}
 
@@ -218,7 +221,6 @@
 end
 *}
 
-
 ML {*
 fun raw_nominal_decls dts bn_funs bn_eqs binds lthy =
 let
@@ -361,10 +363,15 @@
 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy =
 let
   (* definition of the raw datatype and raw bn-functions *)
-  val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_bclauses), raw_bns), lthy1) =
+  val ((((raw_dt_names, (raw_bn_funs, raw_bn_eqs)), raw_bclauses), raw_bns), lthy1) =
     if STEPS > 1 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy
     else raise TEST lthy
 
+  val _ = tracing ("raw_bn_eqs\n" ^ cat_lines (map (@{make_string} o prop_of) raw_bn_eqs))
+  
+  val _ = tracing ("raw_bns\n" ^ @{make_string} raw_bns)
+  val _ = tracing ("raw_bclauses\n" ^ @{make_string} raw_bclauses)
+
   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names);
   val {descr, sorts, ...} = dtinfo;
   val raw_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr;
@@ -373,11 +380,6 @@
 
   val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy1)) all_full_tnames;
   
-  (* what is the difference between raw_dt_names and all_full_tnames ? *)
-  (* what is the purpose of dtinfo and dtinfos ? *)
-  val _ = tracing ("raw_dt_names " ^ commas raw_dt_names)
-  val _ = tracing ("all_full_tnames " ^ commas all_full_tnames)
-
   val inject_thms = flat (map #inject dtinfos);
   val distinct_thms = flat (map #distinct dtinfos);
   val rel_dtinfos = List.take (dtinfos, (length dts)); 
@@ -390,11 +392,11 @@
     if STEPS > 2 then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy1
     else raise TEST lthy1
 
+  (* definition of raw fv_functions *)
   val morphism_2_0 = ProofContext.export_morphism lthy2 lthy
   fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l);
   val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_0)))) raw_bns;
   val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp);
-  val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc
 
   val (_, lthy2a) = Local_Theory.note ((Binding.empty,
     [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), raw_perm_def) lthy2;
@@ -404,9 +406,12 @@
   val lthy3 = Theory_Target.init NONE thy;
   val raw_bn_funs = map (fn (f, _, _) => f) bn_funs_decls;
 
-  (* definition of raw fv_functions *)
+  (*
+  val _ = tracing ("raw_bns\n" ^ @{make_string} raw_bns)
+  val _ = tracing ("raw_bns\n" ^ @{make_string} raw_bns_exp)
+  val _ = tracing ("bn_funs\n" ^ @{make_string} bn_funs_decls)
   val _ = tracing ("raw_bclauses\n" ^ @{make_string} raw_bclauses)
-  val _ = tracing ("raw_bclauses\n" ^ @{make_string} bn_funs_decls)
+  *)
   val ((fv, fvbn), fv_def, lthy3a) = 
     if STEPS > 3 then define_raw_fv descr sorts bn_funs_decls raw_bclauses lthy3
     else raise TEST lthy3