--- a/Nominal/Ex/SingleLet.thy	Tue May 11 18:20:25 2010 +0200
+++ b/Nominal/Ex/SingleLet.thy	Wed May 12 13:43:48 2010 +0100
@@ -16,6 +16,7 @@
 where
   "bn (As x t) = {atom x}"
 
+
 thm trm_assg.fv
 thm trm_assg.supp
 thm trm_assg.eq_iff

--- 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

--- a/Nominal/Perm.thy	Tue May 11 18:20:25 2010 +0200
+++ b/Nominal/Perm.thy	Wed May 12 13:43:48 2010 +0100
@@ -62,6 +62,7 @@
 *}
 
 ML {*
+(* proves the two pt-type class properties *)
 fun prove_permute_zero lthy induct perm_defs perm_fns =
 let
   val perm_types = map (body_type o fastype_of) perm_fns

--- a/Pearl-jv/Paper.thy	Tue May 11 18:20:25 2010 +0200
+++ b/Pearl-jv/Paper.thy	Wed May 12 13:43:48 2010 +0100
@@ -55,10 +55,16 @@
   there are bound term variables and bound type variables; each kind needs to
   be represented by a different sort of atoms.
 
-  Unfortunately, the type system of Isabelle/HOL is not a good fit for the way
-  atoms and sorts are used in the original formulation of the nominal logic work.
-  The reason is that one has to ensure that permutations are sort-respecting.
-  This was done implicitly in the original nominal logic work \cite{Pitts03}.
+  In our formalisation of the nominal logic work, we have to make a design decision 
+  about how to represent sorted atoms and sort-respecting permutations. One possibility
+  is to 
+
+
+
+%  Unfortunately, the type system of Isabelle/HOL is not a good fit for the way
+%  atoms and sorts are used in the original formulation of the nominal logic work.
+%  The reason is that one has to ensure that permutations are sort-respecting.
+%  This was done implicitly in the original nominal logic work \cite{Pitts03}.
 
 
   Isabelle used the two-place permutation operation with the generic type