# HG changeset patch
# User wenzelm
# Date 1139255987 -3600
# Node ID de38ee3654d4ca6bc26b6f82b4f438302019833a
# Parent  ce65d2d2e0c204ecc24a024cb6a2c9b0c594724d
eq_prop: Envir.beta_eta_contract;

diff -r ce65d2d2e0c2 -r de38ee3654d4 src/Pure/Isar/calculation.ML
--- 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;