eq_prop: Envir.beta_eta_contract;

--- a/src/Pure/Isar/calculation.ML	Mon Feb 06 20:59:46 2006 +0100
+++ b/src/Pure/Isar/calculation.ML	Mon Feb 06 20:59:47 2006 +0100
@@ -128,7 +128,7 @@
 fun calculate prep_rules final raw_rules int state =
   let
     val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of;
-    val eq_prop = op aconv o pairself (Pattern.eta_contract o strip_assums_concl);
+    val eq_prop = op aconv o pairself (Envir.beta_eta_contract o strip_assums_concl);
     fun projection ths th = Library.exists (Library.curry eq_prop th) ths;
 
     val opt_rules = Option.map (prep_rules state) raw_rules;