--- a/Nominal/Parser.thy	Thu Mar 04 15:15:44 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 04 15:55:53 2010 +0100
@@ -209,6 +209,21 @@
 
 ML {* add_primrec_wrapper *}
 
+lemma equivp_hack: "equivp x"
+sorry
+ML {*
+fun equivp_hack ctxt rel =
+let
+  val thy = ProofContext.theory_of ctxt
+  val ty = domain_type (fastype_of rel)
+  val cty = ctyp_of thy ty
+  val ct = cterm_of thy rel
+in
+  Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack}
+end
+*}
+
+
 ML {* 
 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy =
 let
@@ -249,12 +264,13 @@
   val alpha_cases = #elims alpha
   val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases lthy4
   val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc
-  val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
+(*  val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt perms (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
   val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc perms
     ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) induct lthy5;
   val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms
     (raw_perm_def @ alpha_inj_loc) alpha_induct_loc lthy6;
   val alpha_eqvt = ProofContext.export lthy6 lthy2 alpha_eqvt_loc;
+  val alpha_equivp_loc = map (equivp_hack lthy6) alpha_ts_loc
   val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc
     inject alpha_inj_loc distinct alpha_cases alpha_eqvt_loc lthy6;
   val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc;
@@ -299,11 +315,15 @@
   val (_, lthy16) = Local_Theory.note ((Binding.name (q_name ^ "_fv"), []), q_fv) lthy15;
   val q_bn = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy16, th))) raw_bn_eqs;
   val (_, lthy17) = Local_Theory.note ((Binding.name (q_name ^ "_bn"), []), q_bn) lthy16;
+  val inj_unfolded = map (LocalDefs.unfold lthy17 @{thms alpha_gen}) alpha_inj
+  val q_inj_pre = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy17, th))) inj_unfolded;
+  val q_inj = map (LocalDefs.fold lthy17 @{thms alpha_gen}) q_inj_pre
+  val (_, lthy18) = Local_Theory.note ((Binding.name (q_name ^ "_inject"), []), q_inj) lthy17;*)
 in
-  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy17)
+  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4)
 end
 *}
-
+ML fold
 ML name_of_typ
 
 ML {*