eq_prop: Envir.beta_eta_contract;
authorwenzelm
Mon, 06 Feb 2006 20:59:47 +0100
changeset 18947 de38ee3654d4
parent 18946 ce65d2d2e0c2
child 18948 b6b19cc8454f
eq_prop: Envir.beta_eta_contract;
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;