src/HOL/Decision_Procs/Commutative_Ring_Complete.thy

   case (7 x P2 Q2 y R)
   consider "x = 0" | "x = 1" | d where "x = Suc (Suc d)"
     by atomize_elim arith
   then show ?case
   proof cases
-    case x: 1
+    case 1
     with 7 show ?thesis
       by (auto simp add: norm_Pinj_0_False)
   next
     case x: 2
     from 7 have "isnorm R" "isnorm P2"