src/HOL/MicroJava/BV/BVNoTypeError.thy

       frs [simp]: "frs = (stk,loc,C,sig,pc)#frs'" 
       by (clarsimp simp add: neq_Nil_conv) fast
 
     from conforms obtain  ST LT rT maxs maxl ins et where
       hconf:  "G \<turnstile>h hp \<surd>" and
-      class:  "is_class G C" and
+      "class":  "is_class G C" and
       meth:   "method (G, C) sig = Some (C, rT, maxs, maxl, ins, et)" and
       phi:    "Phi C sig ! pc = Some (ST,LT)" and
       frame:  "correct_frame G hp (ST,LT) maxl ins (stk,loc,C,sig,pc)" and
       frames: "correct_frames G hp Phi rT sig frs'"
       by (auto simp add: correct_state_def)

     with eff stk loc pc'
     have "check_instr (ins!pc) G hp stk loc C sig pc maxs frs'"
     proof (cases "ins!pc")
       case (Getfield F C) 
       with app stk loc phi obtain v vT stk' where
-        class: "is_class G C" and
+        "class": "is_class G C" and
         field: "field (G, C) F = Some (C, vT)" and
         stk:   "stk = v # stk'" and
         conf:  "G,hp \<turnstile> v ::\<preceq> Class C"
         apply clarsimp
         apply (blast dest: conf_widen [OF wf])

         assume "v \<noteq> Null" 
         with conf field isRef wf
         have "\<exists>D vs. hp (the_Addr v) = Some (D,vs) \<and> G \<turnstile> D \<preceq>C C" 
           by (auto dest!: non_np_objD)
       }
-      ultimately show ?thesis using Getfield field class stk hconf wf
+      ultimately show ?thesis using Getfield field "class" stk hconf wf
         apply clarsimp
         apply (fastsimp intro: wf_prog_ws_prog
 	  dest!: hconfD widen_cfs_fields oconf_objD)
         done
     next
       case (Putfield F C)
       with app stk loc phi obtain v ref vT stk' where
-        class: "is_class G C" and
+        "class": "is_class G C" and
         field: "field (G, C) F = Some (C, vT)" and
         stk:   "stk = v # ref # stk'" and
         confv: "G,hp \<turnstile> v ::\<preceq> vT" and
         confr: "G,hp \<turnstile> ref ::\<preceq> Class C"
         apply clarsimp

         assume "ref \<noteq> Null" 
         with confr field isRef wf
         have "\<exists>D vs. hp (the_Addr ref) = Some (D,vs) \<and> G \<turnstile> D \<preceq>C C"
           by (auto dest: non_np_objD)
       }
-      ultimately show ?thesis using Putfield field class stk confv
+      ultimately show ?thesis using Putfield field "class" stk confv
         by clarsimp
     next      
       case (Invoke C mn ps)
       with app
       obtain apTs X ST' where