diff -r d1e192124cd6 -r 0a7b4e0384d0 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);