src/Pure/raw_simplifier.ML
changeset 51611 0a7b4e0384d0
parent 51591 e4aeb102ad70
child 51717 9e7d1c139569
     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