# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268300369 -3600
# Node ID 25b02cc185e2abcd43b9d196d9c8df59d7fa1691
# Parent  b452e11e409f5c9e0d6347eed97a7f8441a36e11
build_eqvts no longer requires permutations.

diff -r b452e11e409f -r 25b02cc185e2 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Thu Mar 11 10:22:24 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 11 10:39:29 2010 +0100
@@ -323,13 +323,13 @@
     else alpha_eqvt_tac alpha_induct_loc (raw_perm_def @ alpha_inj_loc) lthy4 1
   val alpha_eqvt_loc = build_alpha_eqvts (List.take (alpha_ts_loc, length perms)) perms alpha_eqvt_tac' lthy4;
   val alpha_eqvt = ProofContext.export lthy4 lthy2 alpha_eqvt_loc;
+  val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
 in
 if !restricted_nominal = 0 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
+  val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc
     ((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;
diff -r b452e11e409f -r 25b02cc185e2 Nominal/Rsp.thy
--- a/Nominal/Rsp.thy	Thu Mar 11 10:22:24 2010 +0100
+++ b/Nominal/Rsp.thy	Thu Mar 11 10:39:29 2010 +0100
@@ -120,16 +120,17 @@
 *)
 
 ML {*
-fun build_eqvts bind funs perms simps induct ctxt =
+fun build_eqvts bind funs simps induct ctxt =
 let
   val pi = Free ("p", @{typ perm});
   val types = map (domain_type o fastype_of) funs;
   val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames (map body_type types));
   val args = map Free (indnames ~~ types);
   val perm_at = @{term "permute :: perm \<Rightarrow> atom set \<Rightarrow> atom set"}
-  fun eqvtc (fnctn, (arg, perm)) =
-    HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm $ pi $ arg)))
-  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ (args ~~ perms))))
+  fun perm_arg arg = Const (@{const_name permute}, @{typ perm} --> fastype_of arg --> fastype_of arg)
+  fun eqvtc (fnctn, arg) =
+    HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm_arg arg $ pi $ arg)))
+  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ args)))
   fun tac _ = (Datatype_Aux.indtac induct indnames THEN_ALL_NEW
     (asm_full_simp_tac (HOL_ss addsimps
       (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ (Nominal_ThmDecls.get_eqvts_raw_thms ctxt) @ simps)))) 1
@@ -195,8 +196,8 @@
 *}
 
 ML {*
-fun build_bv_eqvt perms simps inducts (t, n) =
-  build_eqvts Binding.empty [t] [nth perms n] simps (nth inducts n)
+fun build_bv_eqvt simps inducts (t, n) =
+  build_eqvts Binding.empty [t] simps (nth inducts n)
 *}
 
 end