src/HOL/Ord.ML

--- 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";