src/HOL/Tools/datatype_realizer.ML
changeset 18929 d81435108688
parent 18358 0a733e11021a
child 19806 f860b7a98445
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Mon Feb 06 11:01:28 2006 +0100
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Mon Feb 06 20:58:54 2006 +0100
     1.3 @@ -72,7 +72,7 @@
     1.4                    val rT = List.nth (rec_result_Ts, i);
     1.5                    val vs' = filter_out is_unit vs;
     1.6                    val f = mk_Free "f" (map fastype_of vs' ---> rT) j;
     1.7 -                  val f' = Pattern.eta_contract (list_abs_free
     1.8 +                  val f' = Envir.eta_contract (list_abs_free
     1.9                      (map dest_Free vs, if i mem is then list_comb (f, vs')
    1.10                        else HOLogic.unit));
    1.11                  in (HOLogic.mk_Trueprop (make_pred i rT T (list_comb (f, vs'))