Fixed problem in add_elim_realizer (concerning inductive predicates with
parameters) introduced by last bugfix.

--- a/src/HOL/Tools/inductive_realizer.ML	Sat Apr 26 12:44:29 2003 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Sun Apr 27 22:53:11 2003 +0200
@@ -389,11 +389,11 @@
         val (prem :: prems) = prems_of elim;
         fun reorder1 (p, intr) =
           foldl (fn (t, ((s, _), T)) => all T $ lambda (Free (s, T)) t)
-            (strip_all p, Term.add_vars ([], prop_of intr));
+            (strip_all p, Term.add_vars ([], prop_of intr) \\ params');
         fun reorder2 (intr, i) =
           let
-            val fs1 = term_vars (prop_of intr);
-            val fs2 = Term.add_vars ([], prop_of intr)
+            val fs1 = term_vars (prop_of intr) \\ params;
+            val fs2 = Term.add_vars ([], prop_of intr) \\ params'
           in foldl (fn (t, x) => lambda (Var x) t)
             (list_comb (Bound (i + length fs1), fs1), fs2)
           end;