src/Pure/thm.ML
 changeset 30556 7be15917f3fa parent 30554 73f8bd5f0af8 child 30711 952fdbee1b48
```     1.1 --- a/src/Pure/thm.ML	Tue Mar 17 12:09:43 2009 +0100
1.2 +++ b/src/Pure/thm.ML	Tue Mar 17 12:10:42 2009 +0100
1.3 @@ -1248,16 +1248,16 @@
1.4              Envir.norm_term env (Logic.list_implies (Bs, C)),
1.5          thy_ref = Theory.check_thy thy});
1.6
1.7 -    val (close, Hs, C) = Logic.assum_problems (~1, Bi);
1.8 -    val C' = close C;
1.9 +    val (close, asms, concl) = Logic.assum_problems (~1, Bi);
1.10 +    val concl' = close concl;
1.11      fun addprfs [] _ = Seq.empty
1.12 -      | addprfs (H :: rest) n = Seq.make (fn () => Seq.pull
1.13 +      | addprfs (asm :: rest) n = Seq.make (fn () => Seq.pull
1.14            (Seq.mapp (newth n)
1.15 -            (if Term.could_unify (H, C) then
1.16 -              (Unify.unifiers (thy, Envir.empty maxidx, (close H, C') :: tpairs))
1.17 +            (if Term.could_unify (asm, concl) then
1.18 +              (Unify.unifiers (thy, Envir.empty maxidx, (close asm, concl') :: tpairs))
1.19               else Seq.empty)
1.20              (addprfs rest (n + 1))))
1.21 -  in addprfs Hs 1 end;
1.22 +  in addprfs asms 1 end;
1.23
1.24  (*Solve subgoal Bi of proof state B1...Bn/C by assumption.
1.25    Checks if Bi's conclusion is alpha-convertible to one of its assumptions*)
1.26 @@ -1265,8 +1265,9 @@
1.27    let
1.28      val Thm (der, {thy_ref, maxidx, shyps, hyps, prop, ...}) = state;
1.29      val (tpairs, Bs, Bi, C) = dest_state (state, i);
1.30 +    val (_, asms, concl) = Logic.assum_problems (~1, Bi);
1.31    in
1.32 -    (case find_index Pattern.aeconv (Logic.assum_pairs (~1, Bi)) of
1.33 +    (case find_index (fn asm => Pattern.aeconv (asm, concl)) asms of
1.34        ~1 => raise THM ("eq_assumption", 0, [state])
1.35      | n =>
1.36          Thm (deriv_rule1 (Pt.assumption_proof Bs Bi (n + 1)) der,
1.37 @@ -1531,21 +1532,21 @@
1.38         | eres (A1 :: As) =
1.39             let
1.40               val A = SOME A1;
1.41 -             val (close, Hs, C) = Logic.assum_problems (nlift + 1, A1);
1.42 -             val C' = close C;
1.43 +             val (close, asms, concl) = Logic.assum_problems (nlift + 1, A1);
1.44 +             val concl' = close concl;
1.45               fun tryasms [] _ = Seq.empty
1.46 -               | tryasms (H :: rest) n =
1.47 -                   if Term.could_unify (H, C) then
1.48 -                     let val H' = close H in
1.49 -                       (case Seq.pull (Unify.unifiers (thy, env, (H', C') :: dpairs)) of
1.50 +               | tryasms (asm :: rest) n =
1.51 +                   if Term.could_unify (asm, concl) then
1.52 +                     let val asm' = close asm in
1.53 +                       (case Seq.pull (Unify.unifiers (thy, env, (asm', concl') :: dpairs)) of
1.54                           NONE => tryasms rest (n + 1)
1.55                         | cell as SOME ((_, tpairs), _) =>
1.56 -                           Seq.it_right (addth A (newAs (As, n, [BBi, (C', H')], tpairs)))
1.57 +                           Seq.it_right (addth A (newAs (As, n, [BBi, (concl', asm')], tpairs)))
1.58                               (Seq.make (fn () => cell),
1.59                                Seq.make (fn () => Seq.pull (tryasms rest (n + 1)))))
1.60                       end
1.61                     else tryasms rest (n + 1);
1.62 -           in tryasms Hs 1 end;
1.63 +           in tryasms asms 1 end;
1.64
1.65       (*ordinary resolution*)
1.66       fun res () =
```