1.1 --- a/src/HOL/BNF/Examples/Infinite_Derivation_Trees/Gram_Lang.thy	Fri Oct 12 14:57:56 2012 +0200
     1.2 +++ b/src/HOL/BNF/Examples/Infinite_Derivation_Trees/Gram_Lang.thy	Fri Oct 12 15:52:45 2012 +0200
     1.3 @@ -173,8 +173,12 @@
     1.4  lemma subtr_StepL:
     1.5  assumes r: "root tr1 \<in> ns" and tr12: "Inr tr1 \<in> cont tr2" and s: "subtr ns tr2 tr3"
     1.6  shows "subtr ns tr1 tr3"
     1.7 -apply(rule subtr_trans[OF _ s]) apply(rule Step[of tr2 ns tr1 tr1])
     1.8 -by (metis assms subtr_rootL_in Refl)+
     1.9 +apply(rule subtr_trans[OF _ s])
    1.10 +apply(rule Step[of tr2 ns tr1 tr1])
    1.11 +apply(rule subtr_rootL_in[OF s])
    1.12 +apply(rule Refl[OF r])
    1.13 +apply(rule tr12)
    1.14 +done
    1.15  
    1.16  (* alternative definition: *)
    1.17  inductive subtr2 where
    1.18 @@ -220,8 +224,12 @@
    1.19  lemma subtr2_StepR:
    1.20  assumes r: "root tr3 \<in> ns" and tr23: "Inr tr2 \<in> cont tr3" and s: "subtr2 ns tr1 tr2"
    1.21  shows "subtr2 ns tr1 tr3"
    1.22 -apply(rule subtr2_trans[OF s]) apply(rule Step[of _ _ tr3])
    1.23 -by (metis assms subtr2_rootR_in Refl)+
    1.24 +apply(rule subtr2_trans[OF s])
    1.25 +apply(rule Step[of _ _ tr3])
    1.26 +apply(rule subtr2_rootR_in[OF s])
    1.27 +apply(rule tr23)
    1.28 +apply(rule Refl[OF r])
    1.29 +done
    1.30  
    1.31  lemma subtr_subtr2:
    1.32  "subtr = subtr2"
    1.33 @@ -311,7 +319,7 @@
    1.34  corollary Itr_subtr_cont:
    1.35  "Itr ns tr = {root tr' | tr'. subtr ns tr' tr}"
    1.36  unfolding Itr_def apply safe
    1.37 -  apply (metis (lifting, mono_tags) UnionI inItr_subtr mem_Collect_eq vimageI2)
    1.38 +  apply (metis (lifting, mono_tags) inItr_subtr)
    1.39    by (metis inItr.Base subtr_inItr subtr_rootL_in)
    1.40  
    1.41  
    1.42 @@ -512,7 +520,7 @@
    1.43  "hsubst \<equiv> unfold hsubst_r hsubst_c"
    1.44  
    1.45  lemma finite_hsubst_c: "finite (hsubst_c n)"
    1.46 -unfolding hsubst_c_def by (metis finite_cont)
    1.47 +unfolding hsubst_c_def by (metis (full_types) finite_cont)
    1.48  
    1.49  lemma root_hsubst[simp]: "root (hsubst tr) = root tr"
    1.50  using unfold(1)[of hsubst_r hsubst_c tr] unfolding hsubst_def hsubst_r_def by simp
    1.51 @@ -703,7 +711,7 @@
    1.52    apply(rule exI[of _ g])
    1.53    using f deftr_simps(1) unfolding g_def reg_def apply safe
    1.54      apply (metis (lifting) inItr.Base subtr_inItr subtr_rootL_in)
    1.55 -    by (metis (full_types) inItr_subtr subtr_subtr2)
    1.56 +    by (metis (full_types) inItr_subtr)
    1.57  qed auto
    1.58  
    1.59  lemma reg_root:
    1.60 @@ -823,7 +831,7 @@
    1.61      show ?thesis apply(rule exI[of _ nl]) using path.Base unfolding nl Nil by simp
    1.62    next
    1.63      case (Cons n1 nl2)
    1.64 -    hence p1: "path f nl1" by (metis list.simps nl p_nl path_post)
    1.65 +    hence p1: "path f nl1" by (metis list.simps(3) nl p_nl path_post)
    1.66      show ?thesis
    1.67      proof(cases "n \<in> set nl1")
    1.68        case False
    1.69 @@ -1132,7 +1140,7 @@
    1.70         \<Union> {Fr (ns - {root tr}) tr' | tr'. Inr tr' \<in> cont tr}"
    1.71  unfolding Fr_def
    1.72  using In inFr.Base regular_inFr[OF assms] apply safe
    1.73 -apply (simp, metis (full_types) UnionI mem_Collect_eq)
    1.74 +apply (simp, metis (full_types) mem_Collect_eq)
    1.75  apply simp
    1.76  by (simp, metis (lifting) inFr_Ind_minus insert_Diff)
    1.77