# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268298623 -3600
# Node ID beeaa85c98977f9301863e0070fc654dd697e699
# Parent  406ee11355b88b066272b0fc2522cc8b80f15334
Export tactic out of alpha_eqvt.

diff -r 406ee11355b8 -r beeaa85c9897 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Wed Mar 10 16:59:08 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 11 10:10:23 2010 +0100
@@ -319,7 +319,7 @@
   val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc
 in
 if !restricted_nominal = 0 then
-  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy5)
+  ((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;
@@ -327,8 +327,8 @@
     ((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;
+  fun alpha_eqvt_tac' _ = alpha_eqvt_tac alpha_induct_loc (raw_perm_def @ alpha_inj_loc) lthy6 1
+  val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms alpha_eqvt_tac' 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
diff -r 406ee11355b8 -r beeaa85c9897 Nominal/Rsp.thy
--- a/Nominal/Rsp.thy	Wed Mar 10 16:59:08 2010 +0100
+++ b/Nominal/Rsp.thy	Thu Mar 11 10:10:23 2010 +0100
@@ -176,7 +176,7 @@
 *}
 
 ML {*
-fun build_alpha_eqvts funs perms simps induct ctxt =
+fun build_alpha_eqvts funs perms tac ctxt =
 let
   val pi = Free ("p", @{typ perm});
   val types = map (domain_type o fastype_of) funs;
@@ -188,7 +188,6 @@
     HOLogic.mk_imp (alpha $ arg $ arg2,
       (alpha $ (perm $ pi $ arg) $ (perm $ pi $ arg2)))
   val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc ((funs ~~ perms) ~~ (args ~~ args2))))
-  fun tac _ = alpha_eqvt_tac induct simps ctxt 1
   val thm = Goal.prove ctxt ("p" :: indnames @ indnames2) [] gl tac
 in
   map (fn x => mp OF [x]) (HOLogic.conj_elims thm)