src/Pure/Isar/obtain.ML
changeset 18185 9d51fad6bb1f
parent 18151 32538cf750ca
child 18643 89a7978f90e1
     1.1 --- a/src/Pure/Isar/obtain.ML	Wed Nov 16 17:45:30 2005 +0100
     1.2 +++ b/src/Pure/Isar/obtain.ML	Wed Nov 16 17:45:31 2005 +0100
     1.3 @@ -225,7 +225,7 @@
     1.4          val ps = map dest_Free ts;
     1.5          val asms =
     1.6            Logic.strip_assums_hyp (Logic.nth_prem (1, Thm.prop_of rule))
     1.7 -          |> map (fn asm => (Library.foldl Term.betapply (Term.list_abs (ps, asm), ts), ([], [])));
     1.8 +          |> map (fn asm => (Term.betapplys (Term.list_abs (ps, asm), ts), ([], [])));
     1.9          val _ = conditional (null asms) (fn () =>
    1.10            raise Proof.STATE ("Trivial result -- nothing guessed", state));
    1.11        in