diff -r 821628d16552 -r 9f98751c9628 src/HOL/Tools/function_package/lexicographic_order.ML
--- a/src/HOL/Tools/function_package/lexicographic_order.ML	Thu Oct 11 19:10:17 2007 +0200
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Thu Oct 11 19:10:19 2007 +0200
@@ -215,10 +215,10 @@
 (* prove row :: cell list -> tactic *)
 fun prove_row (Less less_thm :: _) =
     (rtac @{thm "mlex_less"} 1)
-    THEN PRIMITIVE (flip implies_elim less_thm)
+    THEN PRIMITIVE (Thm.elim_implies less_thm)
   | prove_row (LessEq (lesseq_thm, _) :: tail) =
     (rtac @{thm "mlex_leq"} 1)
-    THEN PRIMITIVE (flip implies_elim lesseq_thm)
+    THEN PRIMITIVE (Thm.elim_implies lesseq_thm)
     THEN prove_row tail
   | prove_row _ = sys_error "lexicographic_order"