src/Pure/PIDE/document.ML
changeset 52588 bf90a4e842bc
parent 52587 067f1f950dc8
child 52595 76883c1e1c53
     1.1 --- a/src/Pure/PIDE/document.ML	Thu Jul 11 11:09:23 2013 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Thu Jul 11 11:37:06 2013 +0200
     1.3 @@ -415,7 +415,7 @@
     1.4              (case (lookup_entry node0 command_id, opt_exec) of
     1.5                (SOME (eval0, _), SOME (eval, _)) => Command.same_eval (eval0, eval)
     1.6              | _ => false);
     1.7 -          val assign_update' = assign_update |>
     1.8 +          val assign_update' = assign_update |> same' ?
     1.9              (case opt_exec of
    1.10                SOME (eval, prints) =>
    1.11                  let