[isabelle-dev] AFP still broken (AList vs. Assoc_List)

[Makarius]

In Isabelle/f5c4b49c8c9a and AFP/420dac7d9446 from today the situation of 
various AFP sessions is as bad as some days ago:

Promela FAILED
(see also 
/home/makarius/.isabelle/heaps/polyml-5.5.3_x86-linux/log/Promela)

*** At command "by" (line 1082 of "~/isabelle/afp-devel/thys/Promela/PromelaDatastructures.thy")
*** Failed to finish proof (line 1083 of "~/isabelle/afp-devel/thys/Promela/PromelaDatastructures.thy"):
*** goal (1 subgoal):
***  1. [| lsl = Assoc_List.impl_of ls;
***        delete_aux k (update_with_aux v k (%_. v) (Assoc_List.impl_of ls)) =
***        Assoc_List.impl_of ls |]
***     ==> Assoc_List
***          (AList.delete_aux k
***            (AList.update_with_aux v k (%_. v) (Assoc_List.impl_of ls))) =
***         ls
*** At command "by" (line 1083 of "~/isabelle/afp-devel/thys/Promela/PromelaDatastructures.thy")
*** Failed to finish proof (line 1061 of "~/isabelle/afp-devel/thys/Promela/PromelaDatastructures.thy"):
*** goal (1 subgoal):
***  1. [| lsl = Assoc_List.impl_of ls;
***        update_with_aux v k (%_. v) (Assoc_List.impl_of ls) =
***        Assoc_List.impl_of ls |]
***     ==> Assoc_List
***          (AList.update_with_aux v k (%_. v) (Assoc_List.impl_of ls)) =
***         ls
*** At command "by" (line 1061 of "~/isabelle/afp-devel/thys/Promela/PromelaDatastructures.thy")


I am desparately trying to find a locally stable point to make 
Isabelle2015-RC1 -- the official start for several weeks of testing 
towards Isabelle2015 (May 2015), but it is likely to become June 2015 
instead.


 	Makarius