diff -r 9f1eaab75e8c -r 771b1f6422a8 src/HOL/AxClasses/Lattice/Order.ML
--- a/src/HOL/AxClasses/Lattice/Order.ML	Mon Nov 03 12:22:43 1997 +0100
+++ b/src/HOL/AxClasses/Lattice/Order.ML	Mon Nov 03 12:24:13 1997 +0100
@@ -45,7 +45,7 @@
 (* associativity *)
 
 goalw thy [is_inf_def] "is_inf x y xy & is_inf y z yz & is_inf xy z xyz --> is_inf x yz xyz";
-  by (safe_tac (!claset));
+  by (safe_tac (claset()));
   (*level 1*)
     br (le_trans RS mp) 1;
     be conjI 1;
@@ -79,7 +79,7 @@
 
 
 goalw thy [is_sup_def] "is_sup x y xy & is_sup y z yz & is_sup xy z xyz --> is_sup x yz xyz";
-  by (safe_tac (!claset));
+  by (safe_tac (claset()));
   (*level 1*)
     br (le_trans RS mp) 1;
     be conjI 1;
@@ -155,7 +155,7 @@
   (*==>*)
     by (Fast_tac 1);
   (*<==*)
-    by (safe_tac (!claset));
+    by (safe_tac (claset()));
     by (Step_tac 1);
     be mp 1;
     by (Fast_tac 1);
@@ -166,7 +166,7 @@
   (*==>*)
     by (Fast_tac 1);
   (*<==*)
-    by (safe_tac (!claset));
+    by (safe_tac (claset()));
     by (Step_tac 1);
     be mp 1;
     by (Fast_tac 1);