equal
deleted
inserted
replaced
280 |
280 |
281 fun conclude_history thy = if (history_concluded o the_exec) thy |
281 fun conclude_history thy = if (history_concluded o the_exec) thy |
282 then NONE |
282 then NONE |
283 else thy |
283 else thy |
284 |> (Code_Data.map o apfst) |
284 |> (Code_Data.map o apfst) |
285 ((map_functions o Symtab.map) (fn ((changed, current), history) => |
285 ((map_functions o Symtab.map) (fn _ => fn ((changed, current), history) => |
286 ((false, current), |
286 ((false, current), |
287 if changed then (serial (), current) :: history else history)) |
287 if changed then (serial (), current) :: history else history)) |
288 #> map_history_concluded (K true)) |
288 #> map_history_concluded (K true)) |
289 |> SOME; |
289 |> SOME; |
290 |
290 |