diff -r 409ecb7284dd -r c5b7be27f105 Nominal/Tacs.thy
--- a/Nominal/Tacs.thy	Wed May 12 13:43:48 2010 +0100
+++ b/Nominal/Tacs.thy	Wed May 12 16:08:32 2010 +0200
@@ -56,12 +56,6 @@
 end
 *}
 
-(* An induction for a single relation is "R x y \<Longrightarrow> P x y"
-   but for multiple relations is "(R1 x y \<longrightarrow> P x y) \<and> (R2 a b \<longrightarrow> P2 a b)" *)
-ML {*
-fun rel_indtac induct = (rtac impI THEN' etac induct) ORELSE' rtac induct
-*}
-
 ML {*
 fun prove_by_rel_induct alphas build_goal ind utac inputs ctxt =
 let
@@ -80,7 +74,7 @@
     (fn ((alpha, gl), (l, r)) => HOLogic.mk_imp (alpha $ l $ r, gl)) 
     ((alphas ~~ trm_gls) ~~ (freesl ~~ freesr))
   val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj pgls);
-  fun tac {context,...} = (rel_indtac ind THEN_ALL_NEW split_conj_tac THEN_ALL_NEW
+  fun tac {context,...} = (rtac ind THEN_ALL_NEW split_conj_tac THEN_ALL_NEW
     TRY o rtac @{thm TrueI} THEN_ALL_NEW utac context) 1
   val th_loc = Goal.prove ctxt'' [] [] gl tac
   val ths_loc = HOLogic.conj_elims th_loc