removed unnerving (esp in jedit) and pointless warning
authornipkow
Thu, 04 Apr 2013 10:30:28 +0200
changeset 51611 0a7b4e0384d0
parent 51610 d1e192124cd6
child 51612 6a1e40f9dd55
removed unnerving (esp in jedit) and pointless warning
src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Thu Apr 04 08:10:20 2013 +0200
+++ b/src/Pure/raw_simplifier.ML	Thu Apr 04 10:30:28 2013 +0200
@@ -730,9 +730,7 @@
 fun ss addloop' (name, tac) = ss |>
   map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
     (congs, procs, mk_rews, termless, subgoal_tac,
-     (if AList.defined (op =) loop_tacs name
-      then if_visible ss warning ("Overwriting looper " ^ quote name)
-      else (); AList.update (op =) (name, tac) loop_tacs), solvers));
+     AList.update (op =) (name, tac) loop_tacs, solvers));
 
 fun ss addloop (name, tac) = ss addloop' (name, K tac);