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