src/HOL/Nominal/Examples/Fsub.thy

       have lh_drv_prem1: "\<turnstile> \<Gamma>1 ok" by fact
       have lh_drv_prem2: "S1 closed_in \<Gamma>1" by fact
       have Q_inst: "Top=Q" by fact
       have rh_drv: "\<Gamma>1 \<turnstile> Q <: T" --"rh drv." by fact
       hence "T = Top" using Q_inst by (simp add: S_TopE)
-      thus "\<Gamma>1 \<turnstile> S1 <: T" using top_case[of "\<Gamma>1" "S1" "False" "T"] lh_drv_prem1 lh_drv_prem2 by simp
+      thus "\<Gamma>1 \<turnstile> S1 <: T" using top_case[of "\<Gamma>1" "S1" "False" "T"] lh_drv_prem1 lh_drv_prem2 by blast
     next
       case (S_Var \<Gamma>1 X1 S1 T1) --{* lh drv.: @{term "\<Gamma> \<turnstile> S <: Q \<equiv> \<Gamma>1 \<turnstile> TVar(X1) <: S1"} *}
       have lh_drv_prem1: "\<turnstile> \<Gamma>1 ok" by fact
       have lh_drv_prem2: "(X1,S1)\<in>set \<Gamma>1" by fact
       have IH_inner: "\<And>T. \<Gamma>1 \<turnstile> Q <: T \<Longrightarrow> T1=Q \<Longrightarrow> \<Gamma>1 \<turnstile> S1 <: T" by fact