src/HOL/AxClasses/Lattice/LatMorph.ML
changeset 4091 771b1f6422a8
parent 1899 0075a8d26a80
child 4153 e534c4c32d54
--- a/src/HOL/AxClasses/Lattice/LatMorph.ML	Mon Nov 03 12:22:43 1997 +0100
+++ b/src/HOL/AxClasses/Lattice/LatMorph.ML	Mon Nov 03 12:24:13 1997 +0100
@@ -5,7 +5,7 @@
 (** monotone functions vs. "&&"- / "||"-semi-morphisms **)
 
 goalw thy [is_mono_def] "is_mono f = (ALL x y. f (x && y) [= f x && f y)";
-  by (safe_tac (!claset));
+  by (safe_tac (claset()));
   (*==> (level 1)*)
     by (stac le_inf_eq 1);
     br conjI 1;
@@ -28,7 +28,7 @@
 qed "mono_inf_eq";
 
 goalw thy [is_mono_def] "is_mono f = (ALL x y. f x || f y [= f (x || y))";
-  by (safe_tac (!claset));
+  by (safe_tac (claset()));
   (*==> (level 1)*)
     by (stac ge_sup_eq 1);
     br conjI 1;