diff -r 43c4589a9a78 -r 9d51fad6bb1f src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Wed Nov 16 17:45:30 2005 +0100
+++ b/src/Pure/Isar/obtain.ML	Wed Nov 16 17:45:31 2005 +0100
@@ -225,7 +225,7 @@
         val ps = map dest_Free ts;
         val asms =
           Logic.strip_assums_hyp (Logic.nth_prem (1, Thm.prop_of rule))
-          |> map (fn asm => (Library.foldl Term.betapply (Term.list_abs (ps, asm), ts), ([], [])));
+          |> map (fn asm => (Term.betapplys (Term.list_abs (ps, asm), ts), ([], [])));
         val _ = conditional (null asms) (fn () =>
           raise Proof.STATE ("Trivial result -- nothing guessed", state));
       in