src/HOL/Tools/inductive_realizer.ML
changeset 20951 868120282837
parent 20897 3f8d2834b2c4
child 21022 3634641f9405
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Tue Oct 10 13:59:12 2006 +0200
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Tue Oct 10 13:59:13 2006 +0200
     1.3 @@ -262,7 +262,7 @@
     1.4      val vs1 = map Var (filter_out (fn ((a, _), _) => a mem rvs) xs);
     1.5      val rlzvs = rev (Term.add_vars (prop_of rrule) []);
     1.6      val vs2 = map (fn (ixn, _) => Var (ixn, (the o AList.lookup (op =) rlzvs) ixn)) xs;
     1.7 -    val rs = gen_rems (op = o pairself fst) (rlzvs, xs);
     1.8 +    val rs = subtract (op = o pairself fst) xs rlzvs;
     1.9  
    1.10      fun mk_prf _ [] prf = prf
    1.11        | mk_prf rs ((prem, rprem) :: prems) prf =