# HG changeset patch
# User oheimb
# Date 889704799 -3600
# Node ID 7fcd106cb0ed57e51d7d80a10103a73baf22e1c6
# Parent  0136b5bbe9fe4614f9a637e57c72a4d95e63d42b
addloop: added warning in case of overwriting a looper

diff -r 0136b5bbe9fe -r 7fcd106cb0ed src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Thu Mar 12 12:49:24 1998 +0100
+++ b/src/Provers/simplifier.ML	Thu Mar 12 13:13:19 1998 +0100
@@ -151,8 +151,9 @@
   make_ss (mss, subgoal_tac, [("",tac)], finish_tac, unsafe_finish_tac);
 
 fun (Simpset {mss, subgoal_tac, loop_tacs, finish_tac, unsafe_finish_tac})
-    addloop atac =
-  make_ss (mss, subgoal_tac, overwrite(loop_tacs,atac),
+    addloop tac = make_ss (mss, subgoal_tac, 
+	(case assoc_string (loop_tacs,(fst tac)) of None => () | Some x => 
+	 warning ("overwriting looper "^fst tac); overwrite(loop_tacs,tac)),
            finish_tac, unsafe_finish_tac);
 
 fun (ss as Simpset {mss,subgoal_tac,loop_tacs,finish_tac,unsafe_finish_tac})