# HG changeset patch
# User urbanc
# Date 1134679891 -3600
# Node ID 149cc4126997ed9f4670ab3234482a4658d06c47
# Parent  32833aae901f151750e461efcef6955c28b52a17
there was a small error in the last commit - fixed now

diff -r 32833aae901f -r 149cc4126997 src/HOL/Nominal/Examples/Fsub.thy
--- a/src/HOL/Nominal/Examples/Fsub.thy	Thu Dec 15 21:49:14 2005 +0100
+++ b/src/HOL/Nominal/Examples/Fsub.thy	Thu Dec 15 21:51:31 2005 +0100
@@ -731,7 +731,7 @@
       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