substantial speedup of assumption and elim-resolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in beta-normal form, as do higher term net operations anyway);

--- a/src/Pure/logic.ML	Mon Mar 16 23:39:44 2009 +0100
+++ b/src/Pure/logic.ML	Mon Mar 16 23:52:30 2009 +0100
@@ -65,6 +65,7 @@
   val flatten_params: int -> term -> term
   val list_rename_params: string list * term -> term
   val assum_pairs: int * term -> (term*term)list
+  val assum_problems: int * term -> (term -> term) * term list * term
   val varifyT: typ -> typ
   val unvarifyT: typ -> typ
   val varify: term -> term
@@ -462,6 +463,13 @@
   in  pairrev (Hs,[])
   end;
 
+fun assum_problems (nasms, A) =
+  let
+    val (params, A') = strip_assums_all ([], A)
+    val (Hs, B) = strip_assums_imp (nasms, [], A')
+    fun abspar t = rlist_abs (params, t)
+  in (abspar, rev Hs, B) end;
+
 
 (* global schematic variables *)
 

--- a/src/Pure/thm.ML	Mon Mar 16 23:39:44 2009 +0100
+++ b/src/Pure/thm.ML	Mon Mar 16 23:52:30 2009 +0100
@@ -1247,12 +1247,17 @@
           else (*normalize the new rule fully*)
             Envir.norm_term env (Logic.list_implies (Bs, C)),
         thy_ref = Theory.check_thy thy});
+
+    val (close, Hs, C) = Logic.assum_problems (~1, Bi);
+    val C' = close C;
     fun addprfs [] _ = Seq.empty
-      | addprfs ((t, u) :: apairs) n = Seq.make (fn () => Seq.pull
+      | addprfs (H :: rest) n = Seq.make (fn () => Seq.pull
           (Seq.mapp (newth n)
-            (Unify.unifiers (thy, Envir.empty maxidx, (t, u) :: tpairs))
-            (addprfs apairs (n + 1))))
-  in addprfs (Logic.assum_pairs (~1, Bi)) 1 end;
+            (if Term.could_unify (H, C) then
+              (Unify.unifiers (thy, Envir.empty maxidx, (close H, C') :: tpairs))
+             else Seq.empty)
+            (addprfs rest (n + 1))))
+  in addprfs Hs 1 end;
 
 (*Solve subgoal Bi of proof state B1...Bn/C by assumption.
   Checks if Bi's conclusion is alpha-convertible to one of its assumptions*)
@@ -1520,24 +1525,37 @@
      val env = Envir.empty(Int.max(rmax,smax));
      val BBi = if lifted then strip_assums2(B,Bi) else (B,Bi);
      val dpairs = BBi :: (rtpairs@stpairs);
-     (*elim-resolution: try each assumption in turn.  Initially n=1*)
-     fun tryasms (_, _, _, []) = Seq.empty
-       | tryasms (A, As, n, (t,u)::apairs) =
-          (case Seq.pull(Unify.unifiers(thy, env, (t,u)::dpairs))  of
-              NONE                   => tryasms (A, As, n+1, apairs)
-            | cell as SOME((_,tpairs),_) =>
-                Seq.it_right (addth A (newAs(As, n, [BBi,(u,t)], tpairs)))
-                    (Seq.make(fn()=> cell),
-                     Seq.make(fn()=> Seq.pull (tryasms(A, As, n+1, apairs)))))
-     fun eres [] = raise THM("bicompose: no premises", 0, [orule,state])
-       | eres (A1::As) = tryasms(SOME A1, As, 1, Logic.assum_pairs(nlift+1,A1))
+
+     (*elim-resolution: try each assumption in turn*)
+     fun eres [] = raise THM ("bicompose: no premises", 0, [orule, state])
+       | eres (A1 :: As) =
+           let
+             val A = SOME A1;
+             val (close, Hs, C) = Logic.assum_problems (nlift + 1, A1);
+             val C' = close C;
+             fun tryasms [] _ = Seq.empty
+               | tryasms (H :: rest) n =
+                   if Term.could_unify (H, C) then
+                     let val H' = close H in
+                       (case Seq.pull (Unify.unifiers (thy, env, (H', C') :: dpairs)) of
+                         NONE => tryasms rest (n + 1)
+                       | cell as SOME ((_, tpairs), _) =>
+                           Seq.it_right (addth A (newAs (As, n, [BBi, (C', H')], tpairs)))
+                             (Seq.make (fn () => cell),
+                              Seq.make (fn () => Seq.pull (tryasms rest (n + 1)))))
+                     end
+                   else tryasms rest (n + 1);
+           in tryasms Hs 1 end;
+
      (*ordinary resolution*)
-     fun res(NONE) = Seq.empty
-       | res(cell as SOME((_,tpairs),_)) =
-             Seq.it_right (addth NONE (newAs(rev rAs, 0, [BBi], tpairs)))
-                       (Seq.make (fn()=> cell), Seq.empty)
- in  if eres_flg then eres(rev rAs)
-     else res(Seq.pull(Unify.unifiers(thy, env, dpairs)))
+     fun res () =
+       (case Seq.pull (Unify.unifiers (thy, env, dpairs)) of
+         NONE => Seq.empty
+       | cell as SOME ((_, tpairs), _) =>
+           Seq.it_right (addth NONE (newAs (rev rAs, 0, [BBi], tpairs)))
+             (Seq.make (fn () => cell), Seq.empty));
+ in
+   if eres_flg then eres (rev rAs) else res ()
  end;
 end;