subtract: minor performance tuning;
authorwenzelm
Fri Oct 05 20:10:33 2007 +0200 (2007-10-05)
changeset 248572dde4189a055
parent 24856 f06829479407
child 24858 a3a81e73f552
subtract: minor performance tuning;
src/Pure/interpretation.ML
     1.1 --- a/src/Pure/interpretation.ML	Fri Oct 05 11:16:30 2007 +0200
     1.2 +++ b/src/Pure/interpretation.ML	Fri Oct 05 20:10:33 2007 +0200
     1.3 @@ -35,8 +35,9 @@
     1.4  fun consolidate thy =
     1.5    let
     1.6      val (data, interps) = Interp.get thy;
     1.7 -    val unfinished = map (fn ((f, _), xs) => (f, subtract eq xs data)) interps;
     1.8 -    val finished = map (fn (interp, _) => (interp, data)) interps;
     1.9 +    val unfinished = interps |> map (fn ((f, _), xs) =>
    1.10 +      (f, if eq_list eq (xs, data) then [] else subtract eq xs data));
    1.11 +    val finished = interps |> map (fn (interp, _) => (interp, data));
    1.12    in
    1.13      if forall (null o #2) unfinished then NONE
    1.14      else SOME (thy |> fold_rev (uncurry fold_rev) unfinished |> Interp.put (data, finished))