diff -r 91c0c894e1b4 -r 1af2598b5f7d src/HOL/Tools/function_package/pattern_split.ML
--- a/src/HOL/Tools/function_package/pattern_split.ML	Mon Jun 23 20:00:58 2008 +0200
+++ b/src/HOL/Tools/function_package/pattern_split.ML	Mon Jun 23 23:45:39 2008 +0200
@@ -101,7 +101,7 @@
           let
             val t = Pattern.rewrite_term thy sigma [] feq1
           in
-            fold_rev mk_forall (map Free (frees_in_term ctx t) inter vs') t
+            fold_rev Logic.all (map Free (frees_in_term ctx t) inter vs') t
           end
     in
       map instantiate substs