src/Pure/Isar/calculation.ML

--- a/src/Pure/Isar/calculation.ML	Thu Jan 17 21:04:36 2002 +0100
+++ b/src/Pure/Isar/calculation.ML	Thu Jan 17 21:04:48 2002 +0100
@@ -156,7 +156,7 @@
 
 fun calculate final opt_rules print state =
   let
-    val strip_assums_concl = Logic.strip_assums_concl o #prop o Thm.rep_thm;
+    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);
     fun projection ths th = Library.exists (Library.curry eq_prop th) ths;