# HG changeset patch
# User wenzelm
# Date 1191607833 -7200
# Node ID 2dde4189a055c02eddeafba053e9b19a28f6b1b9
# Parent  f06829479407e2abd5d6af7e37719bc495855c0a
subtract: minor performance tuning;

diff -r f06829479407 -r 2dde4189a055 src/Pure/interpretation.ML
--- a/src/Pure/interpretation.ML	Fri Oct 05 11:16:30 2007 +0200
+++ b/src/Pure/interpretation.ML	Fri Oct 05 20:10:33 2007 +0200
@@ -35,8 +35,9 @@
 fun consolidate thy =
   let
     val (data, interps) = Interp.get thy;
-    val unfinished = map (fn ((f, _), xs) => (f, subtract eq xs data)) interps;
-    val finished = map (fn (interp, _) => (interp, data)) interps;
+    val unfinished = interps |> map (fn ((f, _), xs) =>
+      (f, if eq_list eq (xs, data) then [] else subtract eq xs data));
+    val finished = interps |> map (fn (interp, _) => (interp, data));
   in
     if forall (null o #2) unfinished then NONE
     else SOME (thy |> fold_rev (uncurry fold_rev) unfinished |> Interp.put (data, finished))