proper comparison of blobs_info (amending illtyped equality from 86a76300137e) -- avoid redundant update of unchanged commands;

--- 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)
     }
   }