src/HOL/Bali/WellForm.thy
changeset 37678 0040bafffdef
parent 35440 bdf8ad377877
child 37956 ee939247b2fb
     1.1 --- a/src/HOL/Bali/WellForm.thy	Thu Jul 01 16:54:42 2010 +0200
     1.2 +++ b/src/HOL/Bali/WellForm.thy	Thu Jul 01 16:54:44 2010 +0200
     1.3 @@ -2168,7 +2168,7 @@
     1.4        by (force dest!: ws_dynmethd accmethd_SomeD)
     1.5      with dynlookup eq_mheads 
     1.6      show ?thesis 
     1.7 -      by (cases emh type: *) (auto)
     1.8 +      by (cases emh type: prod) (auto)
     1.9    next
    1.10      case Iface_methd
    1.11      fix I im
    1.12 @@ -2191,7 +2191,7 @@
    1.13        by (force dest: implmt_methd)
    1.14      with dynlookup eq_mheads
    1.15      show ?thesis 
    1.16 -      by (cases emh type: *) (auto)
    1.17 +      by (cases emh type: prod) (auto)
    1.18    next
    1.19      case Iface_Object_methd
    1.20      fix I sm
    1.21 @@ -2217,7 +2217,7 @@
    1.22                    intro: class_Object [OF wf] intro: that)
    1.23         with dynlookup eq_mheads
    1.24         show ?thesis 
    1.25 -         by (cases emh type: *) (auto)
    1.26 +         by (cases emh type: prod) (auto)
    1.27       next
    1.28         case False
    1.29         with statI
    1.30 @@ -2243,7 +2243,7 @@
    1.31           by (auto dest: implmt_methd)
    1.32         with wf eq_stat resProp dynlookup eq_mheads
    1.33         show ?thesis 
    1.34 -         by (cases emh type: *) (auto intro: widen_trans)
    1.35 +         by (cases emh type: prod) (auto intro: widen_trans)
    1.36       qed
    1.37    next
    1.38      case Array_Object_methd
    1.39 @@ -2256,7 +2256,7 @@
    1.40        by (auto simp add: dynlookup_def dynmethd_C_C)
    1.41      with sm eq_mheads sm 
    1.42      show ?thesis 
    1.43 -      by (cases emh type: *) (auto dest: accmethd_SomeD)
    1.44 +      by (cases emh type: prod) (auto dest: accmethd_SomeD)
    1.45    qed
    1.46  qed
    1.47  declare split_paired_All [simp] split_paired_Ex [simp]