--- a/Nominal/Ex/CoreHaskell.thy	Sun May 16 11:00:44 2010 +0100
+++ b/Nominal/Ex/CoreHaskell.thy	Sun May 16 12:41:27 2010 +0100
@@ -84,7 +84,7 @@
 | "bv_tvs TvsNil = []"
 | "bv_tvs (TvsCons v k t) = (atom v) # bv_tvs t"
 | "bv_cvs CvsNil = []"
-| "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t"
+| "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t"    
 
 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15)
 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp]
@@ -191,13 +191,13 @@
   done
 
 lemma alpha_perm_bn:
-  "alpha_bv pat (permute_bv q pat)"
-  apply(induct pat rule: inducts(9))
+  "alpha_bv pt (permute_bv q pt)"
+  apply(induct pt rule: inducts(9))
   apply(simp_all add:permute_bv eqvts eq_iff alpha_perm_bn1)
   done
 
 lemma ACons_subst:
-  "supp (Abs_lst (bv pat) trm) \<sharp>* q \<Longrightarrow> (ACons pat trm al) = ACons (permute_bv q pat) (q \<bullet> trm) al"
+  "supp (Abs_lst (bv pt) trm) \<sharp>* q \<Longrightarrow> (ACons pt trm al) = ACons (permute_bv q pt) (q \<bullet> trm) al"
   apply (simp only: eq_iff)
   apply (simp add: alpha_perm_bn)
   apply (rule_tac x="q" in exI)
@@ -352,8 +352,8 @@
   and a35: "\<And>trm assoc_lst b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P8 c assoc_lst\<rbrakk> \<Longrightarrow> P7 b (Case trm assoc_lst)"
   and a36: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (Cast trm ty)"
   and a37: "\<And>b. P8 b ANil"
-  and a38: "\<And>pat trm assoc_lst b. \<lbrakk>\<And>c. P9 c pat; \<And>c. P7 c trm; \<And>c. P8 c assoc_lst; set (bv (pat)) \<sharp>* b\<rbrakk>
-    \<Longrightarrow> P8 b (ACons pat trm assoc_lst)"
+  and a38: "\<And>pt trm assoc_lst b. \<lbrakk>\<And>c. P9 c pt; \<And>c. P7 c trm; \<And>c. P8 c assoc_lst; set (bv (pt)) \<sharp>* b\<rbrakk>
+    \<Longrightarrow> P8 b (ACons pt trm assoc_lst)"
   and a39: "\<And>string tvars cvars vars b. \<lbrakk>\<And>c. P11 c tvars; \<And>c. P12 c cvars; \<And>c. P10 c vars\<rbrakk>
     \<Longrightarrow> P9 b (Kpat string tvars cvars vars)"
   and a40: "\<And>b. P10 b VsNil"
@@ -372,12 +372,12 @@
          P6 (f :: 'f :: pt) co_lst \<and>
          P7 (g :: 'g :: {pt,fs}) trm \<and>
          P8 (h :: 'h :: {pt,fs}) assoc_lst \<and>
-         P9 (i :: 'i :: pt) pat \<and>
+         P9 (i :: 'i :: pt) pt \<and>
          P10 (j :: 'j :: pt) vars \<and>
          P11 (k :: 'k :: pt) tvars \<and>
          P12 (l :: 'l :: pt) cvars"
 proof -
-  have a1: "(\<forall>p a. P1 a (p \<bullet> tkind))" and "(\<forall>p b. P2 b (p \<bullet> ckind))" and "(\<forall>p c. P3 c (p \<bullet> ty))" and "(\<forall>p d. P4 d (p \<bullet> ty_lst))" and "(\<forall>p e. P5 e (p \<bullet> co))" and " (\<forall>p f. P6 f (p \<bullet> co_lst))" and "(\<forall>p g. P7 g (p \<bullet> trm))" and "(\<forall>p h. P8 h (p \<bullet> assoc_lst))" and a1:"(\<forall>p q i. P9 i (permute_bv p (q \<bullet> pat)))" and a2:"(\<forall>p q j. P10 j (permute_bv_vs q (p \<bullet> vars)))" and a3:"(\<forall>p q k. P11 k ( permute_bv_tvs q (p \<bullet> tvars)))" and a4:"(\<forall>p q l. P12 l (permute_bv_cvs q (p \<bullet> cvars)))"
+  have a1: "(\<forall>p a. P1 a (p \<bullet> tkind))" and "(\<forall>p b. P2 b (p \<bullet> ckind))" and "(\<forall>p c. P3 c (p \<bullet> ty))" and "(\<forall>p d. P4 d (p \<bullet> ty_lst))" and "(\<forall>p e. P5 e (p \<bullet> co))" and " (\<forall>p f. P6 f (p \<bullet> co_lst))" and "(\<forall>p g. P7 g (p \<bullet> trm))" and "(\<forall>p h. P8 h (p \<bullet> assoc_lst))" and a1:"(\<forall>p q i. P9 i (permute_bv p (q \<bullet> pt)))" and a2:"(\<forall>p q j. P10 j (permute_bv_vs q (p \<bullet> vars)))" and a3:"(\<forall>p q k. P11 k ( permute_bv_tvs q (p \<bullet> tvars)))" and a4:"(\<forall>p q l. P12 l (permute_bv_cvs q (p \<bullet> cvars)))"
     apply (induct rule: tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.inducts)
     apply (tactic {* ALLGOALS (REPEAT o rtac allI) *})
     apply (tactic {* ALLGOALS (TRY o SOLVED' (simp_tac @{simpset} THEN_ALL_NEW resolve_tac @{thms assms} THEN_ALL_NEW asm_full_simp_tac @{simpset})) *})
@@ -637,7 +637,7 @@
     apply (simp add: fresh_star_def fresh_def supp_abs eqvts)
     done
   then have b: "P1 a (0 \<bullet> tkind)" and "P2 b (0 \<bullet> ckind)" "P3 c (0 \<bullet> ty)" and "P4 d (0 \<bullet> ty_lst)" and "P5 e (0 \<bullet> co)" and "P6 f (0 \<bullet> co_lst)" and "P7 g (0 \<bullet> trm)" and "P8 h (0 \<bullet> assoc_lst)" by (blast+)
-  moreover have "P9  i (permute_bv 0 (0 \<bullet> pat))" and "P10 j (permute_bv_vs 0 (0 \<bullet> vars))" and "P11 k (permute_bv_tvs 0 (0 \<bullet> tvars))" and "P12 l (permute_bv_cvs 0 (0 \<bullet> cvars))" using a1 a2 a3 a4 by (blast+)
+  moreover have "P9  i (permute_bv 0 (0 \<bullet> pt))" and "P10 j (permute_bv_vs 0 (0 \<bullet> vars))" and "P11 k (permute_bv_tvs 0 (0 \<bullet> tvars))" and "P12 l (permute_bv_cvs 0 (0 \<bullet> cvars))" using a1 a2 a3 a4 by (blast+)
   ultimately show ?thesis by (simp_all add: permute_bv_zero1 permute_bv_zero2)
 qed
 

--- a/Nominal/NewParser.thy	Sun May 16 11:00:44 2010 +0100
+++ b/Nominal/NewParser.thy	Sun May 16 12:41:27 2010 +0100
@@ -204,22 +204,6 @@
   in
     (dt_index, (bn_fun, (cnstr_head, included)))
   end
-  fun aux2 eq = 
-  let
-    val (lhs, rhs) = eq
-      |> strip_qnt_body "all" 
-      |> HOLogic.dest_Trueprop
-      |> HOLogic.dest_eq
-    val (bn_fun, [cnstr]) = strip_comb lhs
-    val (_, ty) = dest_Free bn_fun
-    val (ty_name, _) = dest_Type (domain_type ty)
-    val dt_index = find_index (fn x => x = ty_name) dt_names
-    val (cnstr_head, cnstr_args) = strip_comb cnstr
-    val rhs_elements = strip_bn_fun rhs
-    val included = map (apfst (fn i => length (cnstr_args) - i - 1)) rhs_elements
-  in
-    (bn_fun, dt_index, (cnstr_head, included))
-  end 
   fun order dts i ts = 
   let
     val dt = nth dts i
@@ -235,13 +219,14 @@
   val ordered' = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) ordered)
 
   val _ = tracing ("eqs\n" ^ cat_lines (map (Syntax.string_of_term lthy) eqs))
-  val _ = tracing ("map eqs\n" ^ @{make_string} (map aux2 eqs))
+  (*val _ = tracing ("map eqs\n" ^ @{make_string} (map aux2 eqs))*)
   val _ = tracing ("ordered'\n" ^ @{make_string} ordered')
 in
   ordered'
 end
 *}
 
+ML {* add_primrec_wrapper *}
 ML {*
 fun raw_nominal_decls dts bn_funs bn_eqs binds lthy =
 let
@@ -271,14 +256,16 @@
   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_bns = prep_bn lthy dt_full_names' raw_dts (map snd raw_bn_eqs)
 
-  val raw_bns = prep_bn lthy dt_full_names' raw_dts (map snd raw_bn_eqs)
+  val (raw_dt_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
+
+  val morphism_2_0 = ProofContext.export_morphism lthy2 lthy
+  fun export_fun f (t, n , l) = (f t, n, map (map (apsnd (Option.map f))) l);
+  val bn_funs_decls = map (export_fun (Morphism.term morphism_2_0)) raw_bns;
 in
-  lthy 
-  |> add_datatype_wrapper raw_dt_names raw_dts 
-  ||>> add_primrec_wrapper raw_bn_funs raw_bn_eqs
-  ||>> pair raw_bclauses
-  ||>> pair raw_bns
+  (raw_dt_names, raw_bn_eqs, raw_bclauses, bn_funs_decls, lthy2)
 end
 *}
 
@@ -388,7 +375,7 @@
 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, raw_bn_eqs)), raw_bclauses), raw_bns), lthy1) =
+  val (raw_dt_names, raw_bn_eqs, raw_bclauses, raw_bns, lthy1) =
     if get_STEPS lthy > 1 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy
     else raise TEST lthy
 
@@ -413,32 +400,25 @@
     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, n , l) = (f t, n, map (map (apsnd (Option.map f))) l);
-  val bn_funs_decls = map (export_fun (Morphism.term morphism_2_0)) raw_bns;
- 
   val (_, lthy2a) = Local_Theory.note ((Binding.empty,
     [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), raw_perm_def) lthy2;
   val thy = Local_Theory.exit_global lthy2a;
   val thy_name = Context.theory_name thy
 
+  (* definition of raw fv_functions *)
   val lthy3 = Theory_Target.init NONE thy;
-  val raw_bn_funs = map (fn (f, _, _) => f) bn_funs_decls;
+  val raw_bn_funs = map (fn (f, _, _) => f) raw_bns;
 
-  val _ = tracing ("raw_bns\n" ^ @{make_string} raw_bns)
-  val _ = tracing ("bn_funs\n" ^ @{make_string} bn_funs_decls)
-   
   val ((fv, fvbn), fv_def, lthy3a) = 
     if get_STEPS lthy > 3 
-    then define_raw_fv descr sorts bn_funs_decls raw_bclauses lthy3
+    then define_raw_fv descr sorts raw_bns raw_bclauses lthy3
     else raise TEST lthy3
   
 
   (* definition of raw alphas *)
   val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) =
     if get_STEPS lthy > 4 
-    then define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy3a
+    then define_raw_alpha dtinfo raw_bns raw_bclauses fv lthy3a
     else raise TEST lthy3a
   
   val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts

--- a/Nominal/ROOT.ML	Sun May 16 11:00:44 2010 +0100
+++ b/Nominal/ROOT.ML	Sun May 16 12:41:27 2010 +0100
@@ -13,7 +13,7 @@
     "Ex/Modules",
     "Ex/ExPS3",
     "Ex/ExPS7",
-    (*"Ex/CoreHaskell",*)
+    "Ex/CoreHaskell",
     "Ex/Test",
     "Manual/Term4"
     ];