diff -r 0035be079bee -r ead82c82da9e src/HOL/Extraction/Higman.thy
--- a/src/HOL/Extraction/Higman.thy	Wed Jun 13 16:43:02 2007 +0200
+++ b/src/HOL/Extraction/Higman.thy	Wed Jun 13 18:30:11 2007 +0200
@@ -146,16 +146,18 @@
   assumes ab: "a \<noteq> b" and bar: "bar xs"
   shows "\<And>ys zs. bar ys \<Longrightarrow> T a xs zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs" using bar
 proof induct
-  fix xs zs assume "good xs" and "T a xs zs"
-  show "bar zs" by (rule bar1) (rule lemma3)
+  fix xs zs assume "T a xs zs" and "good xs"
+  hence "good zs" by (rule lemma3)
+  then show "bar zs" by (rule bar1)
 next
   fix xs ys
   assume I: "\<And>w ys zs. bar ys \<Longrightarrow> T a (w # xs) zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs"
   assume "bar ys"
   thus "\<And>zs. T a xs zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs"
   proof induct
-    fix ys zs assume "good ys" and "T b ys zs"
-    show "bar zs" by (rule bar1) (rule lemma3)
+    fix ys zs assume "T b ys zs" and "good ys"
+    then have "good zs" by (rule lemma3)
+    then show "bar zs" by (rule bar1)
   next
     fix ys zs assume I': "\<And>w zs. T a xs zs \<Longrightarrow> T b (w # ys) zs \<Longrightarrow> bar zs"
     and ys: "\<And>w. bar (w # ys)" and Ta: "T a xs zs" and Tb: "T b ys zs"
@@ -189,8 +191,9 @@
   shows "\<And>zs. xs \<noteq> [] \<Longrightarrow> R a xs zs \<Longrightarrow> bar zs" using bar
 proof induct
   fix xs zs
-  assume "good xs" and "R a xs zs"
-  show "bar zs" by (rule bar1) (rule lemma2)
+  assume "R a xs zs" and "good xs"
+  then have "good zs" by (rule lemma2)
+  then show "bar zs" by (rule bar1)
 next
   fix xs zs
   assume I: "\<And>w zs. w # xs \<noteq> [] \<Longrightarrow> R a (w # xs) zs \<Longrightarrow> bar zs"
@@ -299,7 +302,7 @@
   thus ?case by iprover
 next
   case (bar2 ws)
-  have "is_prefix (f (length ws) # ws) f" by simp
+  from bar2.prems have "is_prefix (f (length ws) # ws) f" by simp
   thus ?case by (iprover intro: bar2)
 qed