# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1267797379 -3600
# Node ID 39e687a99549c8fa8aef1f17da5770ce1a269cba
# Parent  8d2667ebe26c964e69daca2dac46f5afde91a8e3# Parent  998b1bde64e7bc730de9c2282ea0ed1c446e41ad
merge

diff -r 8d2667ebe26c -r 39e687a99549 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Fri Mar 05 13:04:47 2010 +0100
+++ b/Nominal/Parser.thy	Fri Mar 05 14:56:19 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
@@ -267,9 +268,16 @@
   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;
@@ -325,13 +333,15 @@
   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 (_, 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 *)