Modified eqvt_tac to avoid failure due to introduction rules
whose premises contain variables that do not occur in the
conclusion.

--- a/src/HOL/Nominal/nominal_inductive.ML	Fri Apr 20 15:13:06 2007 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Fri Apr 20 16:11:17 2007 +0200
@@ -346,12 +346,11 @@
            Sign.string_of_term (theory_of_thm intr)
              (Logic.unvarify (prop_of intr)) ^ "\n" ^ s);
         val res = SUBPROOF (fn {prems, ...} =>
-          let val prems' = map (fn th' =>
-            if null (names inter term_consts (prop_of th')) then th' RS th
-            else th') prems
-          in (rtac intr THEN_ALL_NEW
-            (resolve_tac prems ORELSE'
-              (cut_facts_tac prems' THEN' full_simp_tac eqvt_ss))) 1
+          let val prems' = map (fn th' => Simplifier.simplify eqvt_ss
+            (if null (names inter term_consts (prop_of th')) then th' RS th
+             else th')) prems
+            (* FIXME: instantiate intr? *)
+          in (rtac intr THEN_ALL_NEW resolve_tac prems') 1
           end) ctxt 1 st
       in
         case (Seq.pull res handle THM (s, _, _) => eqvt_err s) of