diff -r a608f83e3421 -r 5d7a7e439cec src/HOL/AxClasses/Lattice/OrdDefs.ML
--- a/src/HOL/AxClasses/Lattice/OrdDefs.ML	Tue Jan 30 15:19:20 1996 +0100
+++ b/src/HOL/AxClasses/Lattice/OrdDefs.ML	Tue Jan 30 15:24:36 1996 +0100
@@ -58,7 +58,7 @@
 (*"'a dual" is even an isotype*)
 goal thy "Rep_dual (Abs_dual y) = y";
   br Abs_dual_inverse 1;
-  by (rewrite_goals_tac [dual_def]);
+  by (rewtac dual_def);
   by (fast_tac set_cs 1);
 qed "Abs_dual_inverse'";