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 () =