diff -r dd3b9c046c7d -r 4da5c5c29009 Nominal-General/nominal_eqvt.ML
--- a/Nominal-General/nominal_eqvt.ML	Thu Jun 03 15:02:52 2010 +0200
+++ b/Nominal-General/nominal_eqvt.ML	Mon Jun 07 11:43:01 2010 +0200
@@ -28,66 +28,6 @@
   (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt));
 
 
-(** 
- given the theorem F[t]; proves the theorem F[f t] 
-
-  - F needs to be monotone
-  - f returns either SOME for a term it fires on 
-    and NONE elsewhere 
-**)
-fun map_term f t = 
-  (case f t of
-     NONE => map_term' f t 
-   | x => x)
-and map_term' f (t $ u) = 
-    (case (map_term f t, map_term f u) of
-        (NONE, NONE) => NONE
-      | (SOME t'', NONE) => SOME (t'' $ u)
-      | (NONE, SOME u'') => SOME (t $ u'')
-      | (SOME t'', SOME u'') => SOME (t'' $ u''))
-  | map_term' f (Abs (s, T, t)) = 
-      (case map_term f t of
-        NONE => NONE
-      | SOME t'' => SOME (Abs (s, T, t'')))
-  | map_term' _ _  = NONE;
-
-fun map_thm_tac ctxt tac thm =
-let
-  val monos = Inductive.get_monos ctxt
-  val simps = HOL_basic_ss addsimps @{thms split_def}
-in
-  EVERY [cut_facts_tac [thm] 1, etac rev_mp 1, 
-    REPEAT_DETERM (FIRSTGOAL (simp_tac simps THEN' resolve_tac monos)),
-    REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))]
-end
-
-fun map_thm ctxt f tac thm =
-let
-  val opt_goal_trm = map_term f (prop_of thm)
-in
-  case opt_goal_trm of
-    NONE => thm
-  | SOME goal =>
-     Goal.prove ctxt [] [] goal (fn _ => map_thm_tac ctxt tac thm) 
-end
-
-(*
- inductive premises can be of the form
- R ... /\ P ...; split_conj picks out
- the part P ...
-*)
-fun transform_prem ctxt names thm =
-let
-  fun split_conj names (Const ("op &", _) $ f1 $ f2) = 
-      (case head_of f1 of
-         Const (name, _) => if member (op =) names name then SOME f2 else NONE
-       | _ => NONE)
-  | split_conj _ _ = NONE;
-in
-  map_thm ctxt (split_conj names) (etac conjunct2 1) thm
-end
-
-
 (** equivariance tactics **)
 
 val perm_boolE = @{thm permute_boolE}
@@ -104,7 +44,7 @@
   eqvt_strict_tac ctxt [] pred_names THEN'
   SUBPROOF (fn {prems, context as ctxt, ...} =>
     let
-      val prems' = map (transform_prem ctxt pred_names) prems
+      val prems' = map (transform_prem2 ctxt pred_names) prems
       val tac1 = resolve_tac prems'
       val tac2 = EVERY' [ rtac pi_intro_rule, 
             eqvt_strict_tac ctxt perm_cancel pred_names, resolve_tac prems' ]