--- a/Nominal/Parser.thy	Sun Mar 07 21:30:12 2010 +0100
+++ b/Nominal/Parser.thy	Sun Mar 07 21:30:57 2010 +0100
@@ -223,8 +223,9 @@
 end
 *}
 
+ML {* val restricted_nominal=ref true *}
 
-ML {* 
+ML {*
 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy =
 let
   val thy = ProofContext.theory_of lthy
@@ -240,8 +241,10 @@
   val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) (map fst descr)
   val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;
   val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy2)) all_full_tnames;
+  val rel_dtinfos = List.take (dtinfos, (length dts));
   val inject = flat (map #inject dtinfos);
   val distinct = flat (map #distinct dtinfos);
+  val rel_distinct = map #distinct rel_dtinfos;
   val induct = #induct dtinfo;
   val inducts = #inducts dtinfo;
   val ((raw_perm_def, raw_perm_simps, perms), lthy3) =
@@ -261,18 +264,26 @@
   val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys;
   val bns = raw_bn_funs ~~ bn_nos;
   val alpha_intros = #intrs alpha;
-  val alpha_cases = #elims alpha
-  val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases lthy4
+  val alpha_cases_loc = #elims alpha
+  val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc
+  val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases_loc 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;
+in
+if !restricted_nominal then
+  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4)
+else
+let
+  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 raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts)
+  val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc;
   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;
+    inject alpha_inj_loc distinct alpha_cases_loc alpha_eqvt_loc lthy6;
   val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc;
   val qty_binds = map (fn (_, b, _, _) => b) dts;
   val qty_names = map Name.of_binding qty_binds;
@@ -318,13 +329,19 @@
   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;*)
+  val (_, lthy18) = Local_Theory.note ((Binding.name (q_name ^ "_inject"), []), q_inj) lthy17;
+  val rel_dists = flat (map (distinct_rel lthy18 alpha_cases)
+    (rel_distinct ~~ (List.take (alpha_ts, (length dts)))))
+  val q_dis = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy18, th))) rel_dists;
+  val (_, lthy19) = Local_Theory.note ((Binding.name (q_name ^ "_distinct"), []), q_dis) lthy18;
+  val q_eqvt = map (fn th => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy19, th))) raw_fv_bv_eqvt;
+  val (_, lthy20) = Local_Theory.note ((Binding.empty,
+    [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19;
 in
-  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy4)
+  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy20)
+end
 end
 *}
-ML fold
-ML name_of_typ
 
 ML {* 
 (* parsing the datatypes and declaring *)