src/HOL/Tools/inductive_realizer.ML
changeset 18929 d81435108688
parent 18728 6790126ab5f6
child 19046 bc5c6c9b114e
--- a/src/HOL/Tools/inductive_realizer.ML	Mon Feb 06 11:01:28 2006 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Mon Feb 06 20:58:54 2006 +0100
@@ -336,7 +336,7 @@
         end
       else ((recs, dummies), replicate (length rs) Extraction.nullt))
         ((get #rec_thms dt_info, dummies), rss);
-    val rintrs = map (fn (intr, c) => Pattern.eta_contract
+    val rintrs = map (fn (intr, c) => Envir.eta_contract
       (Extraction.realizes_of thy2 vs
         c (prop_of (forall_intr_list (map (cterm_of (sign_of thy2) o Var)
           (rev (Term.add_vars (prop_of intr) []) \\ params')) intr))))