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