src/HOL/Bali/WellForm.thy

       "is_static dm = is_static sm" 
       "G\<turnstile>resTy dm\<preceq>resTy sm"  
       by (force dest!: ws_dynmethd accmethd_SomeD)
     with dynlookup eq_mheads 
     show ?thesis 
-      by (cases emh type: *) (auto)
+      by (cases emh type: prod) (auto)
   next
     case Iface_methd
     fix I im
     assume    statI: "statT = IfaceT I" and
           eq_mheads: "mthd im = mhd emh" and

       "is_static dm = is_static im" 
       "G\<turnstile>resTy (mthd dm)\<preceq>resTy (mthd im)" 
       by (force dest: implmt_methd)
     with dynlookup eq_mheads
     show ?thesis 
-      by (cases emh type: *) (auto)
+      by (cases emh type: prod) (auto)
   next
     case Iface_Object_methd
     fix I sm
     assume   statI: "statT = IfaceT I" and
                 sm: "accmethd G S Object sig = Some sm" and 

          "G\<turnstile>resTy (mthd dm)\<preceq>resTy (mthd sm)"  
          by (auto dest!: ws_dynmethd accmethd_SomeD 
                   intro: class_Object [OF wf] intro: that)
        with dynlookup eq_mheads
        show ?thesis 
-         by (cases emh type: *) (auto)
+         by (cases emh type: prod) (auto)
      next
        case False
        with statI
        have dynlookup: "dynlookup G statT dynC sig = methd G dynC sig"
          by (simp add: dynlookup_def dynimethd_def)

          "is_static dm = is_static im" 
          "G\<turnstile>resTy (mthd dm)\<preceq>resTy (mthd im)" 
          by (auto dest: implmt_methd)
        with wf eq_stat resProp dynlookup eq_mheads
        show ?thesis 
-         by (cases emh type: *) (auto intro: widen_trans)
+         by (cases emh type: prod) (auto intro: widen_trans)
      qed
   next
     case Array_Object_methd
     fix T sm
     assume statArr: "statT = ArrayT T" and

     from statArr dynC_Prop wf
     have dynlookup: "dynlookup G statT dynC sig = methd G Object sig"
       by (auto simp add: dynlookup_def dynmethd_C_C)
     with sm eq_mheads sm 
     show ?thesis 
-      by (cases emh type: *) (auto dest: accmethd_SomeD)
+      by (cases emh type: prod) (auto dest: accmethd_SomeD)
   qed
 qed
 declare split_paired_All [simp] split_paired_Ex [simp]
 declaration {* K (Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))) *}
 declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}