src/HOL/MicroJava/BV/LBVComplete.thy

   have stepA: "snd`set ?step \<subseteq> A" by (rule pres_typeD2) 
   ultimately
   have "merge c pc ?step (c!Suc pc) =
     (if \<forall>(pc',s')\<in>set ?step. pc'\<noteq>pc+1 \<longrightarrow> s' <=_r c!pc'
     then map snd [(p',t') \<leftarrow> ?step.p'=pc+1] ++_f c!Suc pc
-    else \<top>)" unfolding merge_def by (rule lbv.merge_def [OF lbvc.axioms(1), OF lbvc_axioms])
+    else \<top>)" unfolding mrg_def by (rule lbv.merge_def [OF lbvc.axioms(1), OF lbvc_axioms])
   moreover {
     fix pc' s' assume s': "(pc', s') \<in> set ?step" and suc_pc: "pc' \<noteq> pc+1"
     with less have "s' <=_r \<phi>!pc'" by auto
     also 
     from bounded pc s' have "pc' < length \<phi>" by (rule boundedD)