src/Pure/meta_simplifier.ML
changeset 21286 b5e7b80caa6a
parent 20972 db0425645cc7
child 21516 c2a116a2c4fd
     1.1 --- a/src/Pure/meta_simplifier.ML	Fri Nov 10 07:37:37 2006 +0100
     1.2 +++ b/src/Pure/meta_simplifier.ML	Fri Nov 10 07:44:47 2006 +0100
     1.3 @@ -320,7 +320,7 @@
     1.4      [Pretty.big_list "simplification rules:" (pretty_thms smps),
     1.5        Pretty.big_list "simplification procedures:" (map pretty_proc prcs),
     1.6        Pretty.big_list "congruences:" (map pretty_cong cngs),
     1.7 -      Pretty.strs ("loopers:" :: map (quote o #1) loop_tacs),
     1.8 +      Pretty.strs ("loopers:" :: map (quote o fst) loop_tacs),
     1.9        Pretty.strs ("unsafe solvers:" :: map (quote o solver_name) (#1 solvers)),
    1.10        Pretty.strs ("safe solvers:" :: map (quote o solver_name) (#2 solvers))]
    1.11      |> Pretty.chunks |> Pretty.writeln
    1.12 @@ -688,18 +688,20 @@
    1.13  fun ss addloop' (name, tac) = ss |>
    1.14    map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
    1.15      (congs, procs, mk_rews, termless, subgoal_tac,
    1.16 -      overwrite_warn (loop_tacs, (name, tac)) ("Overwriting looper " ^ quote name),
    1.17 +      (if AList.defined (op =) loop_tacs name
    1.18 +        then warning ("Overwriting looper " ^ quote name)
    1.19 +        else (); AList.update (op =) (name, tac) loop_tacs),
    1.20        solvers));
    1.21  
    1.22  fun ss addloop (name, tac) = ss addloop' (name, K tac);
    1.23  
    1.24  fun ss delloop name = ss |>
    1.25    map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
    1.26 -    let val loop_tacs' = filter_out (equal name o fst) loop_tacs in
    1.27 -      if length loop_tacs <> length loop_tacs' then ()
    1.28 -      else warning ("No such looper in simpset: " ^ quote name);
    1.29 -      (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs', solvers)
    1.30 -    end);
    1.31 +    (congs, procs, mk_rews, termless, subgoal_tac,
    1.32 +      (if AList.defined (op =) loop_tacs name
    1.33 +        then ()
    1.34 +        else warning ("No such looper in simpset: " ^ quote name);
    1.35 +       AList.delete (op =) name loop_tacs), solvers));
    1.36  
    1.37  fun ss setSSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
    1.38    subgoal_tac, loop_tacs, (unsafe_solvers, _)) =>
    1.39 @@ -759,7 +761,7 @@
    1.40      val congs' = gen_merge_lists (eq_cong o pairself #2) congs1 congs2;
    1.41      val weak' = merge_lists weak1 weak2;
    1.42      val procs' = Net.merge eq_proc (procs1, procs2);
    1.43 -    val loop_tacs' = merge_alists loop_tacs1 loop_tacs2;
    1.44 +    val loop_tacs' = AList.merge (op =) (K true) (loop_tacs1, loop_tacs2);
    1.45      val unsafe_solvers' = merge_solvers unsafe_solvers1 unsafe_solvers2;
    1.46      val solvers' = merge_solvers solvers1 solvers2;
    1.47    in