Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
subtract: minor performance tuning;
authorwenzelm
Fri, 05 Oct 2007 20:10:33 +0200
changeset 24857 2dde4189a055
parent 24856 f06829479407
child 24858 a3a81e73f552
subtract: minor performance tuning;
src/Pure/interpretation.ML file | annotate | diff | comparison | revisions 
--- 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))
isabelle