differ: compare actual props only (hyps may changed due to trivial steps involving assumptions);
authorwenzelm
Tue Sep 21 17:07:28 1999 +0200 (1999-09-21)
changeset 755430327f9f6b4a
parent 7553 af3a1fe87c42
child 7555 dd281afb33d7
differ: compare actual props only (hyps may changed due to trivial steps involving assumptions);
src/Pure/Isar/calculation.ML
     1.1 --- a/src/Pure/Isar/calculation.ML	Tue Sep 21 17:06:49 1999 +0200
     1.2 +++ b/src/Pure/Isar/calculation.ML	Tue Sep 21 17:07:28 1999 +0200
     1.3 @@ -125,7 +125,8 @@
     1.4      val facts = Proof.the_facts state;
     1.5      val rules = Seq.of_list (if_none opt_rules [] @ get_local_rules state);
     1.6  
     1.7 -    fun differ thms thms' = not (Library.equal_lists Thm.eq_thm (thms, thms'));
     1.8 +    val eq_prop = op aconv o pairself (#prop o Thm.rep_thm);
     1.9 +    fun differ thms thms' = not (Library.equal_lists eq_prop (thms, thms'));
    1.10      fun combine thms =
    1.11        Seq.map Library.single (Seq.flat (Seq.map (Method.multi_resolve (thms @ facts)) rules));
    1.12