diff -r 5cf13e80be0e -r 502a7c95de73 src/HOL/Hyperreal/Lim.ML
--- a/src/HOL/Hyperreal/Lim.ML	Thu Nov 27 10:47:55 2003 +0100
+++ b/src/HOL/Hyperreal/Lim.ML	Fri Nov 28 12:09:37 2003 +0100
@@ -1661,7 +1661,7 @@
 by (asm_full_simp_tac (simpset() addsimps []) 1);
 by (dres_inst_tac [("x","s")] spec 1);
 by (Clarify_tac 1);
-by (cut_inst_tac [("R1.0","f x"),("R2.0","y")] real_linear 1);
+by (cut_inst_tac [("x","f x"),("y","y")] linorder_less_linear 1);
 by Safe_tac;
 by (dres_inst_tac [("x","ba - x")] spec 1);
 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [abs_iff])));