diff -r ecf6375e2abb -r 426ed18eba43 src/Pure/Isar/auto_bind.ML
--- a/src/Pure/Isar/auto_bind.ML	Sat Jan 14 20:05:58 2012 +0100
+++ b/src/Pure/Isar/auto_bind.ML	Sat Jan 14 21:16:15 2012 +0100
@@ -26,7 +26,7 @@
 fun strip_judgment thy = Object_Logic.drop_judgment thy o Logic.strip_assums_concl;
 
 fun statement_binds thy name prop =
-  [((name, 0), SOME (Term.list_abs (Logic.strip_params prop, strip_judgment thy prop)))];
+  [((name, 0), SOME (fold_rev Term.abs (Logic.strip_params prop) (strip_judgment thy prop)))];
 
 
 (* goal *)
@@ -39,7 +39,7 @@
 
 fun get_arg thy prop =
   (case strip_judgment thy prop of
-    _ $ t => SOME (Term.list_abs (Logic.strip_params prop, t))
+    _ $ t => SOME (fold_rev Term.abs (Logic.strip_params prop) t)
   | _ => NONE);
 
 fun facts _ [] = []