Strange. The proof worked in the 2008 release. In order to make it work now, the last line of the proof must be moved up two places. In other words, the first proof step is now returning its subgoals in a different order from before.

--- a/src/HOL/UNITY/Comp/Progress.thy	Fri Nov 21 07:34:36 2008 +0100
+++ b/src/HOL/UNITY/Comp/Progress.thy	Fri Nov 21 13:17:43 2008 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/UNITY/Transformers
+(*  Title:      HOL/UNITY/Progress
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   2003  University of Cambridge
@@ -93,12 +93,9 @@
 apply (subgoal_tac "FF\<squnion>GG \<in> (atLeast 0 \<inter> atLeast 0) leadsTo atLeast k")
  apply simp
 apply (rule_tac T = "atLeast 0" in leadsTo_Join)
-oops
-(* FIXME rotten proof
-  apply (simp add: awp_iff_constrains FF_def, safety)
- apply (simp add: awp_iff_constrains GG_def wens_set_FF, safety)
-apply (rule leadsTo_weaken_L [OF FF_leadsTo], simp) 
+  apply (rule leadsTo_weaken_L [OF FF_leadsTo], simp) 
+ apply (simp add: awp_iff_constrains FF_def, safety)
+apply (simp add: awp_iff_constrains GG_def wens_set_FF, safety)
 done
-*)
 
 end