# HG changeset patch
# User wenzelm
# Date 1427236625 -3600
# Node ID 88a89f01fc27952499f2fe8dea0e515860e50075
# Parent  684cfaa12e47b09fac97fe80d93c95128279e565
proper comparison of blobs_info (amending illtyped equality from 86a76300137e) -- avoid redundant update of unchanged commands;

diff -r 684cfaa12e47 -r 88a89f01fc27 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Tue Mar 24 21:54:25 2015 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Tue Mar 24 23:37:05 2015 +0100
@@ -147,8 +147,8 @@
     : (List[Command], List[(Command.Blobs_Info, Command_Span.Span)]) =
   {
     (cmds, blobs_spans) match {
-      case (cmd :: cmds, (blobs, span) :: rest) if cmd.blobs == blobs && cmd.span == span =>
-        chop_common(cmds, rest)
+      case (cmd :: cmds, (blobs_info, span) :: rest)
+      if cmd.blobs_info == blobs_info && cmd.span == span => chop_common(cmds, rest)
       case _ => (cmds, blobs_spans)
     }
   }