--- a/src/HOL/AxClasses/Lattice/OrdDefs.ML Mon Nov 03 12:22:43 1997 +0100
+++ b/src/HOL/AxClasses/Lattice/OrdDefs.ML Mon Nov 03 12:24:13 1997 +0100
@@ -13,7 +13,7 @@
qed "le_prod_refl";
goalw thy [le_prod_def] "x [= y & y [= z --> x [= (z::'a::quasi_order*'b::quasi_order)";
- by (safe_tac (!claset));
+ by (safe_tac (claset()));
be (conjI RS (le_trans RS mp)) 1;
ba 1;
be (conjI RS (le_trans RS mp)) 1;
@@ -21,7 +21,7 @@
qed "le_prod_trans";
goalw thy [le_prod_def] "x [= y & y [= x --> x = (y::'a::partial_order*'b::partial_order)";
- by (safe_tac (!claset));
+ by (safe_tac (claset()));
by (stac Pair_fst_snd_eq 1);
br conjI 1;
be (conjI RS (le_antisym RS mp)) 1;
@@ -39,13 +39,13 @@
qed "le_fun_refl";
goalw thy [le_fun_def] "f [= g & g [= h --> f [= (h::'a=>'b::quasi_order)";
- by (safe_tac (!claset));
+ by (safe_tac (claset()));
br (le_trans RS mp) 1;
by (Fast_tac 1);
qed "le_fun_trans";
goalw thy [le_fun_def] "f [= g & g [= f --> f = (g::'a=>'b::partial_order)";
- by (safe_tac (!claset));
+ by (safe_tac (claset()));
br ext 1;
br (le_antisym RS mp) 1;
by (Fast_tac 1);
@@ -73,7 +73,7 @@
qed "le_dual_trans";
goalw thy [le_dual_def] "x [= y & y [= x --> x = (y::'a::partial_order dual)";
- by (safe_tac (!claset));
+ by (safe_tac (claset()));
br (Rep_dual_inverse RS subst) 1;
br sym 1;
br (Rep_dual_inverse RS subst) 1;