eq_prop: eta contract;
authorwenzelm
Mon Jun 26 23:59:29 2000 +0200 (2000-06-26)
changeset 915345f8896faacd
parent 9152 034cb4ac78b8
child 9154 e71460b18988
eq_prop: eta contract;
src/Pure/Isar/calculation.ML
     1.1 --- a/src/Pure/Isar/calculation.ML	Mon Jun 26 16:54:38 2000 +0200
     1.2 +++ b/src/Pure/Isar/calculation.ML	Mon Jun 26 23:59:29 2000 +0200
     1.3 @@ -125,7 +125,7 @@
     1.4    let
     1.5      val facts = Proof.the_facts state;
     1.6  
     1.7 -    val eq_prop = op aconv o pairself (#prop o Thm.rep_thm);
     1.8 +    val eq_prop = op aconv o pairself (Pattern.eta_contract o #prop o Thm.rep_thm);
     1.9      fun differ thms thms' = not (Library.equal_lists eq_prop (thms, thms'));
    1.10  
    1.11      fun combine thms =