--- a/src/Pure/thm.ML Mon Dec 11 21:09:24 2023 +0100
+++ b/src/Pure/thm.ML Mon Dec 11 21:17:28 2023 +0100
@@ -2375,15 +2375,15 @@
(*Modify assumptions, deleting n-th if n>0 for e-resolution*)
fun newAs (As0, n, dpairs, tpairs) =
let val (As1, rder') =
- if not lifted then (As0, rder)
- else
+ if lifted then
(case rename_bvars dpairs tpairs B As0 of
- NONE => (As0, rder)
- | SOME f =>
+ SOME f =>
let
fun proof p = Same.commit (Proofterm.map_proof_terms_same f I) p;
fun zproof p = ZTerm.todo_proof p;
- in (map (strip_apply (Same.commit f) B) As0, deriv_rule1 zproof proof rder) end);
+ in (map (strip_apply (Same.commit f) B) As0, deriv_rule1 zproof proof rder) end
+ | NONE => (As0, rder))
+ else (As0, rder);
in
(if flatten then map (Logic.flatten_params n) As1 else As1, As1, rder', n)
handle TERM _ => raise THM("bicompose: 1st premise", 0, [orule])