diff -r 340df9f3491f -r 22f665a2e91c src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy
--- a/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy	Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy	Mon Sep 12 07:55:43 2011 +0200
@@ -110,7 +110,7 @@
   js \<noteq> {} \<Longrightarrow> (\<And>js'. js' \<in> iseq xs (Suc i) \<Longrightarrow> Max js' = i \<Longrightarrow> finite js' \<Longrightarrow>
     js' \<noteq> {} \<Longrightarrow> card js' \<le> card js) \<Longrightarrow>
   j = liseq' xs i"
-  by (fastsimp simp add: liseq'_def iseq_finite
+  by (fastforce simp add: liseq'_def iseq_finite
     intro: Max_eqI [symmetric])
 
 lemma liseq_ge:
@@ -122,7 +122,7 @@
   (\<And>js'. js' \<in> iseq xs i \<Longrightarrow> finite js' \<Longrightarrow>
     js' \<noteq> {} \<Longrightarrow> card js' \<le> card js) \<Longrightarrow>
   j = liseq xs i"
-  by (fastsimp simp add: liseq_def iseq_finite
+  by (fastforce simp add: liseq_def iseq_finite
     intro: Max_eqI [symmetric])
 
 lemma max_notin: "finite xs \<Longrightarrow> Max xs < x \<Longrightarrow> x \<notin> xs"