--- a/src/HOLCF/IOA/NTP/Correctness.ML Fri May 16 16:14:58 1997 +0200
+++ b/src/HOLCF/IOA/NTP/Correctness.ML Fri May 16 17:14:55 1997 +0200
@@ -77,7 +77,7 @@
by (Action.action.induct_tac "a" 1);
by (asm_simp_tac (ss' setloop (split_tac [expand_if])) 1);
by (forward_tac [inv4] 1);
-by (fast_tac (!claset unsafe_addss (!simpset addsimps [neq_Nil_conv])) 1);
+by (fast_tac (!claset addss (!simpset addsimps [neq_Nil_conv])) 1);
by (simp_tac ss' 1);
by (simp_tac ss' 1);
by (simp_tac ss' 1);
@@ -91,7 +91,7 @@
by (forward_tac [inv2] 1);
by (etac disjE 1);
by (Asm_simp_tac 1);
-by (fast_tac (!claset unsafe_addss (!simpset addsimps [neq_Nil_conv])) 1);
+by (fast_tac (!claset addss (!simpset addsimps [neq_Nil_conv])) 1);
by (asm_simp_tac ss' 1);
by (forward_tac [inv2] 1);
@@ -105,7 +105,7 @@
by (case_tac "m = hd(sq(sen(s)))" 1);
-by (fast_tac (!claset unsafe_addss (!simpset addsimps [neq_Nil_conv])) 1);
+by (fast_tac (!claset addss (!simpset addsimps [neq_Nil_conv])) 1);
by (Asm_full_simp_tac 1);
by (fast_tac (!claset addSDs [add_leD1 RS leD]) 1);