diff -r 3e068ef04b42 -r 6d2a2f0e904e src/HOL/UNITY/Lift_prog.thy
--- a/src/HOL/UNITY/Lift_prog.thy	Tue Mar 13 21:17:37 2012 +0100
+++ b/src/HOL/UNITY/Lift_prog.thy	Tue Mar 13 22:49:02 2012 +0100
@@ -301,7 +301,7 @@
     "[| F i \<in> (A <*> UNIV) co (B <*> UNIV);   
         F j \<in> preserves snd |]   
      ==> lift j (F j) \<in> (lift_set i (A <*> UNIV)) co (lift_set i (B <*> UNIV))"
-apply (case_tac "i=j")
+apply (cases "i=j")
 apply (simp add: lift_def lift_set_def rename_constrains)
 apply (erule preserves_snd_lift_stable[THEN stableD, THEN constrains_weaken_R],
        assumption)