Fixed problem in add_elim_realizer (concerning inductive predicates with
authorberghofe
Sun Apr 27 22:53:11 2003 +0200 (2003-04-27)
changeset 13928d572aeea3ff3
parent 13927 6643b8808812
child 13929 21615e44ba88
Fixed problem in add_elim_realizer (concerning inductive predicates with
parameters) introduced by last bugfix.
src/HOL/Tools/inductive_realizer.ML
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Sat Apr 26 12:44:29 2003 +0200
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sun Apr 27 22:53:11 2003 +0200
     1.3 @@ -389,11 +389,11 @@
     1.4          val (prem :: prems) = prems_of elim;
     1.5          fun reorder1 (p, intr) =
     1.6            foldl (fn (t, ((s, _), T)) => all T $ lambda (Free (s, T)) t)
     1.7 -            (strip_all p, Term.add_vars ([], prop_of intr));
     1.8 +            (strip_all p, Term.add_vars ([], prop_of intr) \\ params');
     1.9          fun reorder2 (intr, i) =
    1.10            let
    1.11 -            val fs1 = term_vars (prop_of intr);
    1.12 -            val fs2 = Term.add_vars ([], prop_of intr)
    1.13 +            val fs1 = term_vars (prop_of intr) \\ params;
    1.14 +            val fs2 = Term.add_vars ([], prop_of intr) \\ params'
    1.15            in foldl (fn (t, x) => lambda (Var x) t)
    1.16              (list_comb (Bound (i + length fs1), fs1), fs2)
    1.17            end;