src/Pure/Isar/calculation.ML
changeset 12805 3be853cf19cf
parent 12402 cef751fff6b0
child 13371 82a057cf4413
     1.1 --- a/src/Pure/Isar/calculation.ML	Thu Jan 17 21:04:36 2002 +0100
     1.2 +++ b/src/Pure/Isar/calculation.ML	Thu Jan 17 21:04:48 2002 +0100
     1.3 @@ -156,7 +156,7 @@
     1.4  
     1.5  fun calculate final opt_rules print state =
     1.6    let
     1.7 -    val strip_assums_concl = Logic.strip_assums_concl o #prop o Thm.rep_thm;
     1.8 +    val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of;
     1.9      val eq_prop = op aconv o pairself (Pattern.eta_contract o strip_assums_concl);
    1.10      fun projection ths th = Library.exists (Library.curry eq_prop th) ths;
    1.11