diff -r 91c0c894e1b4 -r 1af2598b5f7d src/HOL/Tools/function_package/context_tree.ML
--- a/src/HOL/Tools/function_package/context_tree.ML	Mon Jun 23 20:00:58 2008 +0200
+++ b/src/HOL/Tools/function_package/context_tree.ML	Mon Jun 23 23:45:39 2008 +0200
@@ -177,7 +177,7 @@
 
 fun export_term (fixes, assumes) =
     fold_rev (curry Logic.mk_implies o prop_of) assumes 
- #> fold_rev (mk_forall o Free) fixes
+ #> fold_rev (Logic.all o Free) fixes
 
 fun export_thm thy (fixes, assumes) =
     fold_rev (implies_intr o cprop_of) assumes