# HG changeset patch
# User berghofe
# Date 1051476791 -7200
# Node ID d572aeea3ff3ea9ea4621e73f1267c598a1adc66
# Parent  6643b8808812b8788a25857f28e951b0546e2a00
Fixed problem in add_elim_realizer (concerning inductive predicates with
parameters) introduced by last bugfix.

diff -r 6643b8808812 -r d572aeea3ff3 src/HOL/Tools/inductive_realizer.ML
--- 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;