--- a/src/HOL/Ord.ML Mon Nov 03 12:12:10 1997 +0100
+++ b/src/HOL/Ord.ML Mon Nov 03 12:13:18 1997 +0100
@@ -25,12 +25,12 @@
AddIffs [order_refl];
goal Ord.thy "~ x < (x::'a::order)";
-by (simp_tac (!simpset addsimps [order_less_le]) 1);
+by (simp_tac (simpset() addsimps [order_less_le]) 1);
qed "order_less_irrefl";
AddIffs [order_less_irrefl];
goal thy "(x::'a::order) <= y = (x < y | x = y)";
-by (simp_tac (!simpset addsimps [order_less_le]) 1);
+by (simp_tac (simpset() addsimps [order_less_le]) 1);
by (Blast_tac 1);
qed "order_le_less";
@@ -46,5 +46,5 @@
by (cut_facts_tac prems 1);
by (split_tac [expand_if] 1);
by (Asm_simp_tac 1);
-by (blast_tac (!claset addIs [order_antisym]) 1);
+by (blast_tac (claset() addIs [order_antisym]) 1);
qed "min_leastR";