src/Pure/Isar/code.ML
changeset 39020 ac0f24f850c9
parent 38667 8494cb38cbf7
child 39134 917b4b6ba3d2
equal deleted inserted replaced
39019:bfd0c0e4dbee 39020:ac0f24f850c9
   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