--- a/src/Pure/Isar/calculation.ML Wed Nov 26 16:55:43 2014 +0100
+++ b/src/Pure/Isar/calculation.ML Wed Nov 26 20:05:34 2014 +0100
@@ -135,7 +135,7 @@
val pretty_thm_item = Display.pretty_thm_item ctxt;
val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of;
- val eq_prop = op aconv o pairself (Envir.beta_eta_contract o strip_assums_concl);
+ val eq_prop = op aconv o apply2 (Envir.beta_eta_contract o strip_assums_concl);
fun check_projection ths th =
(case find_index (curry eq_prop th) ths of
~1 => Seq.Result [th]