# HG changeset patch
# User oheimb
# Date 856025711 -3600
# Node ID 6c6a44b5f7576fffda0b28c6ecafec50e24922db
# Parent  e9b203f854ae11f90c593ce356652edfe4005f5c
reflecting my recent changes of the classical reasoner

diff -r e9b203f854ae -r 6c6a44b5f757 src/HOL/IOA/NTP/Correctness.ML
--- a/src/HOL/IOA/NTP/Correctness.ML	Sat Feb 15 17:52:31 1997 +0100
+++ b/src/HOL/IOA/NTP/Correctness.ML	Sat Feb 15 17:55:11 1997 +0100
@@ -78,7 +78,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 addss (!simpset addsimps [neq_Nil_conv])) 1);
+by (fast_tac (!claset unsafe_addss (!simpset addsimps [neq_Nil_conv])) 1);
 by (simp_tac ss' 1);
 by (simp_tac ss' 1);
 by (simp_tac ss' 1);
@@ -92,7 +92,7 @@
 by (forward_tac [inv2] 1);
 by (etac disjE 1);
 by (Asm_simp_tac 1);
-by (fast_tac (!claset addss (!simpset addsimps [neq_Nil_conv])) 1);
+by (fast_tac (!claset unsafe_addss (!simpset addsimps [neq_Nil_conv])) 1);
 
 by (asm_simp_tac ss' 1);
 by (forward_tac [inv2] 1);
@@ -106,7 +106,7 @@
 
 by (case_tac "m = hd(sq(sen(s)))" 1);
 
-by (fast_tac (!claset addss (!simpset addsimps [neq_Nil_conv])) 1);
+by (fast_tac (!claset unsafe_addss (!simpset addsimps [neq_Nil_conv])) 1);
 
 by (Asm_full_simp_tac 1);
 by (fast_tac (!claset addSDs [add_leD1 RS leD]) 1);