src/HOL/Tools/function_package/context_tree.ML

--- a/src/HOL/Tools/function_package/context_tree.ML	Thu Oct 11 19:10:17 2007 +0200
+++ b/src/HOL/Tools/function_package/context_tree.ML	Thu Oct 11 19:10:19 2007 +0200
@@ -196,7 +196,7 @@
 
 fun import_thm thy (fixes, athms) =
     fold (forall_elim o cterm_of thy o Free) fixes
- #> fold (flip implies_elim) athms
+ #> fold Thm.elim_implies athms
 
 fun assume_in_ctxt thy (fixes, athms) prop =
     let