src/Pure/Isar/calculation.ML
changeset 9322 b5bd2709a2c2
parent 9217 adef902823f9
child 9900 8035a13c61a0
     1.1 --- a/src/Pure/Isar/calculation.ML	Thu Jul 13 23:16:48 2000 +0200
     1.2 +++ b/src/Pure/Isar/calculation.ML	Thu Jul 13 23:17:14 2000 +0200
     1.3 @@ -125,7 +125,8 @@
     1.4    let
     1.5      val facts = Proof.the_facts state;
     1.6  
     1.7 -    val eq_prop = op aconv o pairself (Pattern.eta_contract o #prop o Thm.rep_thm);
     1.8 +    val strip_assums_concl = Logic.strip_assums_concl o #prop o Thm.rep_thm;
     1.9 +    val eq_prop = op aconv o pairself (Pattern.eta_contract o strip_assums_concl);
    1.10      fun differ thms thms' = not (Library.equal_lists eq_prop (thms, thms'));
    1.11  
    1.12      fun combine thms =
    1.13 @@ -134,7 +135,7 @@
    1.14          val rs = get_local_rules state;
    1.15          val rules =
    1.16            (case ths of [] => NetRules.rules rs
    1.17 -          | th :: _ => NetRules.may_unify rs (Logic.strip_assums_concl (#prop (Thm.rep_thm th))));
    1.18 +          | th :: _ => NetRules.may_unify rs (strip_assums_concl th));
    1.19          val ruleq = Seq.of_list (if_none opt_rules [] @ rules);
    1.20        in Seq.map Library.single (Seq.flat (Seq.map (Method.multi_resolve ths) ruleq)) end;
    1.21