# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268302514 -3600
# Node ID 5d421b327f79fa242c2900eddbd9f732d46752ca
# Parent  25b02cc185e2abcd43b9d196d9c8df59d7fa1691
extract build_eqvts_tac.

diff -r 25b02cc185e2 -r 5d421b327f79 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Thu Mar 11 10:39:29 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 11 11:15:14 2010 +0100
@@ -326,11 +326,11 @@
   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)
+  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy5)
 else
 let
   val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc
-    ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) induct lthy5;
+    (build_eqvts_tac induct ((flat (map snd bv_eqvts)) @ fv_def_loc @ raw_perm_def) lthy5) 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_equivp_loc = map (equivp_hack lthy6) alpha_ts_loc
diff -r 25b02cc185e2 -r 5d421b327f79 Nominal/Rsp.thy
--- a/Nominal/Rsp.thy	Thu Mar 11 10:39:29 2010 +0100
+++ b/Nominal/Rsp.thy	Thu Mar 11 11:15:14 2010 +0100
@@ -120,7 +120,17 @@
 *)
 
 ML {*
-fun build_eqvts bind funs simps induct ctxt =
+fun ind_tac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct
+*}
+
+ML {*
+fun build_eqvts_tac induct simps ctxt inds _ = (Datatype_Aux.indtac induct inds 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
+*}
+
+ML {*
+fun build_eqvts bind funs tac ctxt =
 let
   val pi = Free ("p", @{typ perm});
   val types = map (domain_type o fastype_of) funs;
@@ -131,10 +141,7 @@
   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
-  val thm = Goal.prove ctxt ("p" :: indnames) [] gl tac
+  val thm = Goal.prove ctxt ("p" :: indnames) [] gl (tac indnames)
   val thms = HOLogic.conj_elims thm
 in
   Local_Theory.note ((bind, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), thms) ctxt
@@ -147,9 +154,6 @@
 by auto
 
 ML {*
-fun ind_tac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct
-*}
-ML {*
   fun all_eqvts ctxt =
     Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt
   val split_conjs = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)
@@ -196,8 +200,8 @@
 *}
 
 ML {*
-fun build_bv_eqvt simps inducts (t, n) =
-  build_eqvts Binding.empty [t] simps (nth inducts n)
+fun build_bv_eqvt simps inducts (t, n) ctxt =
+  build_eqvts Binding.empty [t] (build_eqvts_tac (nth inducts n) simps ctxt) ctxt
 *}
 
 end