# HG changeset patch
# User wenzelm
# Date 963523034 -7200
# Node ID b5bd2709a2c22f8af90703b07045b65f3bcfb6e0
# Parent  e0dda4bde88c8036f28521d0d3778caa57b0f855
eq_prop: strip_assums_concl;

diff -r e0dda4bde88c -r b5bd2709a2c2 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Thu Jul 13 23:16:48 2000 +0200
+++ b/src/Pure/Isar/calculation.ML	Thu Jul 13 23:17:14 2000 +0200
@@ -125,7 +125,8 @@
   let
     val facts = Proof.the_facts state;
 
-    val eq_prop = op aconv o pairself (Pattern.eta_contract o #prop o Thm.rep_thm);
+    val strip_assums_concl = Logic.strip_assums_concl o #prop o Thm.rep_thm;
+    val eq_prop = op aconv o pairself (Pattern.eta_contract o strip_assums_concl);
     fun differ thms thms' = not (Library.equal_lists eq_prop (thms, thms'));
 
     fun combine thms =
@@ -134,7 +135,7 @@
         val rs = get_local_rules state;
         val rules =
           (case ths of [] => NetRules.rules rs
-          | th :: _ => NetRules.may_unify rs (Logic.strip_assums_concl (#prop (Thm.rep_thm th))));
+          | th :: _ => NetRules.may_unify rs (strip_assums_concl th));
         val ruleq = Seq.of_list (if_none opt_rules [] @ rules);
       in Seq.map Library.single (Seq.flat (Seq.map (Method.multi_resolve ths) ruleq)) end;