diff -r 3216d65d8f34 -r a9b6c2ea7bec src/HOL/Tools/Function/function_lib.ML
--- a/src/HOL/Tools/Function/function_lib.ML	Sun Oct 16 16:56:01 2011 +0200
+++ b/src/HOL/Tools/Function/function_lib.ML	Sun Oct 16 18:48:30 2011 +0200
@@ -75,9 +75,7 @@
   let
     val allthm = Thm.forall_intr cv thm
     val (_ $ abs) = prop_of allthm
-  in
-    Thm.rename_boundvars abs (Abs (n, dummyT, Term.dummy_pattern dummyT)) allthm
-  end
+  in Thm.rename_boundvars abs (Abs (n, dummyT, Term.dummy)) allthm end
 
 
 datatype proof_attempt = Solved of thm | Stuck of thm | Fail